Disable verify models if we use optimize values

OCamlPro · Aug 16, 2024 · 0383115 · 0383115
1 parent f6025b6
commit 0383115
Show file tree

Hide file tree

Showing 8 changed files with 13 additions and 5 deletions.
diff --git a/tests/issues/1163.models.smt2 b/tests/issues/1163.models.smt2
@@ -1,5 +1,6 @@
-(set-logic ALL)
 (set-option :produce-models true)
+(set-option :verify-models false)
+(set-logic ALL)
 (declare-const x Int)
 (define-fun myabs ((x Int)) Int (ite (< x 0) (- x) x))
 (maximize (myabs x))

diff --git a/tests/models/arith/arith13.models.smt2 b/tests/models/arith/arith13.models.smt2
@@ -1,5 +1,6 @@
-(set-option :produce-models true)
 (set-logic ALL)
+(set-option :produce-models true)
+(set-option :verify-models false)
 (declare-const x Int)
 (assert (<= x 10))
 (push 1)

diff --git a/tests/models/arith/arith14.models.smt2 b/tests/models/arith/arith14.models.smt2
@@ -1,4 +1,5 @@
 (set-option :produce-models true)
+(set-option :verify-models false)
 (set-logic ALL)
 (declare-const x Int)
 (declare-const y Int)

diff --git a/tests/models/bitv/optim-1.models.smt2 b/tests/models/bitv/optim-1.models.smt2
@@ -1,6 +1,7 @@
 ; Test basic functionality
-(set-logic ALL)
 (set-option :produce-models true)
+(set-option :verify-models false)
+(set-logic ALL)
 (declare-const x (_ BitVec 32))
 (maximize x)
 (check-sat)

diff --git a/tests/models/bitv/optim-2.models.smt2 b/tests/models/bitv/optim-2.models.smt2
@@ -1,6 +1,7 @@
 ; Test primitive optimization
-(set-logic ALL)
 (set-option :produce-models true)
+(set-option :verify-models false)
+(set-logic ALL)
 (declare-const x (_ BitVec 32))
 (minimize (bvnot x))
 (check-sat)

diff --git a/tests/models/bitv/optim-3.models.smt2 b/tests/models/bitv/optim-3.models.smt2
@@ -1,6 +1,7 @@
 ; Test constrained optimization
 (set-logic ALL)
 (set-option :produce-models true)
+(set-option :verify-models false)
 (declare-const x (_ BitVec 32))
 (maximize x)
 (assert (bvslt x ((_ int2bv 32) (- 1))))

diff --git a/tests/models/bitv/optim-4.models.smt2 b/tests/models/bitv/optim-4.models.smt2
@@ -1,6 +1,7 @@
 ; Test constrained function optimization
-(set-logic ALL)
 (set-option :produce-models true)
+(set-option :verify-models false)
+(set-logic ALL)
 (declare-const x (_ BitVec 32))
 (define-fun bvabs32 ((x (_ BitVec 32))) (_ BitVec 33)
   (ite

diff --git a/tests/models/bitv/optim-5.models.smt2 b/tests/models/bitv/optim-5.models.smt2
@@ -1,5 +1,6 @@
 ; Test lexicographic optimization
 (set-option :produce-models true)
+(set-option :verify-models false)
 (set-logic ALL)
 (declare-const x (_ BitVec 32))
 (declare-const y (_ BitVec 32))