From 34949ec2b1dde9a87af107548eb330d42b2a916d Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Fri, 16 Aug 2024 16:57:41 +0200
Subject: [PATCH] Disable verify models if we use optimize values

---
 tests/issues/1163.default.smt2          | 3 ++-
 tests/models/arith/arith13.default.smt2 | 3 ++-
 tests/models/arith/arith14.default.smt2 | 1 +
 tests/models/bitv/optim-1.default.smt2  | 3 ++-
 tests/models/bitv/optim-2.default.smt2  | 3 ++-
 tests/models/bitv/optim-3.default.smt2  | 1 +
 tests/models/bitv/optim-4.default.smt2  | 3 ++-
 tests/models/bitv/optim-5.default.smt2  | 1 +
 8 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/tests/issues/1163.default.smt2 b/tests/issues/1163.default.smt2
index debce6627..8d0988768 100644
--- a/tests/issues/1163.default.smt2
+++ b/tests/issues/1163.default.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.default.smt2 b/tests/models/arith/arith13.default.smt2
index dc248e6bd..d55d12fae 100644
--- a/tests/models/arith/arith13.default.smt2
+++ b/tests/models/arith/arith13.default.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.default.smt2 b/tests/models/arith/arith14.default.smt2
index 1add26986..b3188634e 100644
--- a/tests/models/arith/arith14.default.smt2
+++ b/tests/models/arith/arith14.default.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.default.smt2 b/tests/models/bitv/optim-1.default.smt2
index 2dc349470..da886135d 100644
--- a/tests/models/bitv/optim-1.default.smt2
+++ b/tests/models/bitv/optim-1.default.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.default.smt2 b/tests/models/bitv/optim-2.default.smt2
index 355630137..366d0e636 100644
--- a/tests/models/bitv/optim-2.default.smt2
+++ b/tests/models/bitv/optim-2.default.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.default.smt2 b/tests/models/bitv/optim-3.default.smt2
index 3408a460b..3d08614fb 100644
--- a/tests/models/bitv/optim-3.default.smt2
+++ b/tests/models/bitv/optim-3.default.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.default.smt2 b/tests/models/bitv/optim-4.default.smt2
index fe5e1b341..b1f63be7f 100644
--- a/tests/models/bitv/optim-4.default.smt2
+++ b/tests/models/bitv/optim-4.default.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.default.smt2 b/tests/models/bitv/optim-5.default.smt2
index 57e5a0116..ce7599c43 100644
--- a/tests/models/bitv/optim-5.default.smt2
+++ b/tests/models/bitv/optim-5.default.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))