Clean usage of options in regressions (#8190)

We now support tester annotations, thus it is best practice not to use check-unsat-cores or check-models explicitly in the regressions.

This changes regressions to not use these options, where these options are either:

removed entirely (the benchmark was fixed in the meantime)
changed to -q (the benchmark succeeds with a warning)
changed to produce- instead of check- if the option on the benchmark is required to ensure a configuration of models/unsat-cores is run. This is done for unsat-cores on sat benchmarks and models on unsat benchmarks.
replaced by DISABLE-TESTER: model.
one spurious regression is deleted, which was identical to another + check-models.
It also makes some fixes to enable more benchmarks succeed with check-models, and adds a warning when fmf-fun is combined with check-model.

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 5a410ba2dfbfe1a9d9a82f6fd62c8648e74fe24e..22718ae0474fb54827f7ecd36d00a29ceb287bf1 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -16,6 +16,7 @@
 #include "smt/check_models.h"
 
 #include "base/modal_exception.h"
+#include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
 #include "smt/preprocessor.h"
@@ -47,6 +48,12 @@ void CheckModels::checkModel(TheoryModel* m,
     throw RecoverableModalException(
         "Cannot run check-model on a model with a separation logic heap.");
   }
+  if (options().quantifiers.fmfFunWellDefined)
+  {
+    warning() << "Running check-model is not guaranteed to pass when fmf-fun "
+                 "is enabled."
+              << std::endl;
+  }
 
   theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
   Trace("check-model") << "checkModel: Check assertions..." << std::endl;

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8854db8772d91b533161e0a984e5d75194b2a3b5..555b35a36d5ed770bb756ed1e69278d0c6447d12 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -119,6 +119,7 @@ void TheoryDatatypes::finishInit()
   }
   // testers are not relevant for model building
   d_valuation.setIrrelevantKind(APPLY_TESTER);
+  d_valuation.setIrrelevantKind(DT_SYGUS_BOUND);
 }
 
 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 153d5bc37a3acf8a6a8072a92e4507b983a9eee6..06467a24ac98357752d90ea80f8dc6659ff2af87 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -490,7 +490,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
 
   /* Generate counterexample lemma for 'q'. */
   NodeManager* nm = NodeManager::currentNM();
-  SkolemManager * sm = nm->getSkolemManager();
+  SkolemManager* sm = nm->getSkolemManager();
   TermDbSygus* db = d_treg.getTermDatabaseSygus();
 
   // For each variable x_i of \forall x_i . P[x_i], create a fresh datatype

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a4921e5c96f117f5c9623cd1c137bc96c739b091..cc52cc126b4f034308e9efef41f8ac0ed3fa550e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -211,7 +211,6 @@ set(regress_0_tests
   regress0/bug383.smt2
   regress0/bug398.smt2
   regress0/bug421.smt2
-  regress0/bug421b.smt2
   regress0/bug480.smt2
   regress0/bug484.smt2
   regress0/bug486.cvc.smt2

diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2
index c9a84d1ec38279d72f8f1ae4098ff588231ac051..99bedad3a062fa8a842a8f4cacc4c60480835436 100644 (file)
--- a/test/regress/regress0/arith/bug569.smt2
+++ b/test/regress/regress0/arith/bug569.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; timeout with unsat cores
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2
index 14af6b6ad77e50a2d14ba23d04fcaabc74cadf12..50ff90e221b202a203013c59c76a866908a35066 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann4.smt2
+++ b/test/regress/regress0/arith/integers/ackermann4.smt2
@@ -1,5 +1,7 @@
-; COMMAND-LINE: --ackermann --no-check-unsat-cores
+; COMMAND-LINE: --ackermann
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; unsat cores throws error in debug mode
 (set-logic QF_ALIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
@@ -19,4 +21,4 @@
 (assert (= v0 v1))
 
 (check-sat)
-(exit)
\ No newline at end of file
+(exit)

diff --git a/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 b/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2
index 3f23e0367235055b4717b65d3b80833e56ef0756..11734fbc66025e97c5ecba1ff1d08c13e477b939 100644 (file)
--- a/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2
+++ b/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -i --check-models
+; COMMAND-LINE: -i
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat

diff --git a/test/regress/regress0/arith/issue4367.smt2 b/test/regress/regress0/arith/issue4367.smt2
index abe5b09fd27bf8fbbb973463ff05664fd7e4857f..52e15a36671f431bc29a0b7226a0401092100666 100644 (file)
--- a/test/regress/regress0/arith/issue4367.smt2
+++ b/test/regress/regress0/arith/issue4367.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --check-unsat-cores
+; COMMAND-LINE: --incremental
 ; EXPECT: unsat
 ; EXPECT: unsat
 (set-logic NRA)

diff --git a/test/regress/regress0/arrays/issue3813-massign-assert.smt2 b/test/regress/regress0/arrays/issue3813-massign-assert.smt2
index 7de7aebc8ab70357c089080738c768af4b1d598d..2e71b26d56005811a7d75d46c153c83f5560cfa9 100644 (file)
--- a/test/regress/regress0/arrays/issue3813-massign-assert.smt2
+++ b/test/regress/regress0/arrays/issue3813-massign-assert.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --check-unsat-cores
+; COMMAND-LINE: --produce-unsat-cores
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun a () (Array Int Bool))

diff --git a/test/regress/regress0/arrays/issue4414.smt2 b/test/regress/regress0/arrays/issue4414.smt2
index d84041fc9b830b4179333803b4496f89f614d8aa..757c14b918bf2b2a913cd86ce5ac9ee277a8b0f6 100644 (file)
--- a/test/regress/regress0/arrays/issue4414.smt2
+++ b/test/regress/regress0/arrays/issue4414.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --check-models --check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_AUFLIA)
 (declare-const a (Array Int Int))

diff --git a/test/regress/regress0/arrays/issue4927-unsat-cores.smt2 b/test/regress/regress0/arrays/issue4927-unsat-cores.smt2
index ad967b48fd3424967dd70a78a4abf5995cd2318d..5532d39d22a39abf2421c3ca0fd2a55cbccfd8da 100644 (file)
--- a/test/regress/regress0/arrays/issue4927-unsat-cores.smt2
+++ b/test/regress/regress0/arrays/issue4927-unsat-cores.smt2
@@ -1,4 +1,4 @@
-; COMMANDLINE: --check-unsat-cores --check-models
+; COMMAND-LINE: --produce-models
 ; EXPECT: unsat
 (set-logic QF_AX)
 (declare-const a (Array Bool Bool))

diff --git a/test/regress/regress0/arrays/issue5720.smt2 b/test/regress/regress0/arrays/issue5720.smt2
index 8d0f81f80245a622ee4cc66301a0066e78d52131..5fc4d828bca78155171e65affa33d7bd67818d58 100644 (file)
--- a/test/regress/regress0/arrays/issue5720.smt2
+++ b/test/regress/regress0/arrays/issue5720.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: -i
 ; EXPECT: unsat
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALIA)
 (set-option :check-unsat-cores true)
 (set-option :fmf-fun true)

diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
index 88cbd8a0ba2d31ebe58727328af7606535ad62a1..fefb3c059f85b626cb1dbb712293be3af2aa3a39 100644 (file)
--- a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
+++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --check-models
 ; EXPECT: sat
 (set-logic QF_AUFBV)
 (declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))

diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2
deleted file mode 100644 (file)
index 72942a2..0000000
--- a/test/regress/regress0/bug421b.smt2
+++ /dev/null
@@ -1,14 +0,0 @@
-; same as bug421.smt2 but adds --check-models on command line:
-; this actually caused the same bug for a different reason, so
-; we check them both independently in regressions
-;
-; COMMAND-LINE: --incremental --abstract-values --check-models
-; EXPECT: sat
-; EXPECT: ((a (as @a_1 (Array Int Int))) (b (as @a_2 (Array Int Int))))
-(set-logic QF_AUFLIA)
-(set-option :produce-models true)
-(declare-fun a () (Array Int Int))
-(declare-fun b () (Array Int Int))
-(assert (not (= a b)))
-(check-sat)
-(get-value (a b))

diff --git a/test/regress/regress0/bug528a.smt2 b/test/regress/regress0/bug528a.smt2
index 97b891415c5165af1ad81ea16359ba40dbac903c..7f2d0deceb8658df98b58cd1135365bfc0089e38 100644 (file)
--- a/test/regress/regress0/bug528a.smt2
+++ b/test/regress/regress0/bug528a.smt2
@@ -1,5 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --incremental --repeat-simp --no-check-unsat-cores
+; COMMAND-LINE: --incremental --repeat-simp
+; DISABLE-TESTER: unsat-core
 (set-logic QF_LIA)
 (declare-fun i () Int)
 (assert (ite (= i 0) false true))

diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index f70dc4a3d05e22ac26d78393ce72f2d40502e33d..545f558f29d96b485f12ed870ef1a6876f12f38b 100644 (file)
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -1,6 +1,7 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models 
-; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal --no-check-models 
+; COMMAND-LINE: --bitblast=eager 
+; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal 
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2
index 8eb5ca70ac012f170ee9fef242104087177263ae..3893c2e7b20d70551d9d402901e9b16e6dd33d2a 100644 (file)
--- a/test/regress/regress0/bv/ackermann3.smt2
+++ b/test/regress/regress0/bv/ackermann3.smt2
@@ -1,5 +1,7 @@
-; COMMAND-LINE: --bitblast=eager --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; unsat cores throws error in debug
 (set-logic QF_ABV)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2
index ad65d8ca406f7cbc25dd73815e3fdc8daaf50f38..3e4898d454c3e70717c0aff7451d79d85f00ee45 100644 (file)
--- a/test/regress/regress0/bv/ackermann4.smt2
+++ b/test/regress/regress0/bv/ackermann4.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models
+; COMMAND-LINE: --bitblast=eager
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2
index dc2cb7f357c696948e69c573c9aa503dcad8923a..03ff10903f98dc6d603825e47c2cc9e6e244e623 100644 (file)
--- a/test/regress/regress0/bv/bv_to_int_5281.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5281.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --check-models --incremental
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :check-models true)

diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index eced6e0e96a549078a7b36897c888d3f4765c2e4..614e2bb1683005a74c445122c8553a0d109fbfb0 100644 (file)
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))

diff --git a/test/regress/regress0/bv/int_to_bv_model.smt2 b/test/regress/regress0/bv/int_to_bv_model.smt2
index ebe8ab10c041d449210cd41830a8dd4548efbb78..c139c78580cf4eedc23a7ccf1e9221624443fd66 100644 (file)
--- a/test/regress/regress0/bv/int_to_bv_model.smt2
+++ b/test/regress/regress0/bv/int_to_bv_model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=9 --check-models
+; COMMAND-LINE: --solve-int-as-bv=9
 ; EXPECT: sat
 (set-logic QF_NIA)
 (declare-const a Int)

diff --git a/test/regress/regress0/bv/int_to_bv_model2.smt2 b/test/regress/regress0/bv/int_to_bv_model2.smt2
index d4ad9695f8d5bc9e6bd23c6075f80562d05dd0c9..b3f4c6e802a66fa2dc130e7c538e8f6104bc6c7e 100644 (file)
--- a/test/regress/regress0/bv/int_to_bv_model2.smt2
+++ b/test/regress/regress0/bv/int_to_bv_model2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=5 --check-models
+; COMMAND-LINE: --solve-int-as-bv=5
 (set-logic QF_NIA)
 (set-info :status sat)
 (declare-const x Int)

diff --git a/test/regress/regress0/bv/proj-issue343.smt2 b/test/regress/regress0/bv/proj-issue343.smt2
index 6d2971ad8aff6122f6b6941143b1fe1d994ef8d5..307cd1a49c82c7460ec020df1abbc4a935cc4cb9 100644 (file)
--- a/test/regress/regress0/bv/proj-issue343.smt2
+++ b/test/regress/regress0/bv/proj-issue343.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE: -q
 (set-logic ALL)
 (set-option :solve-bv-as-int bv)
 (declare-const _x8 Real)

diff --git a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 b/test/regress/regress0/bv/test-bv_intro_pow2.smt2
index 65471a6b93b148ee91ab4107ed90cacbfc28686a..1900ddcb100d576084d0114c0a23d976196d0156 100644 (file)
--- a/test/regress/regress0/bv/test-bv_intro_pow2.smt2
+++ b/test/regress/regress0/bv/test-bv_intro_pow2.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores
+; COMMAND-LINE: --bv-intro-pow2
+; DISABLE-TESTER: unsat-core
 (set-info :smt-lib-version 2.6)
 (set-logic QF_BV)
 (set-info :status unsat)

diff --git a/test/regress/regress0/cores/issue4971-0.smt2 b/test/regress/regress0/cores/issue4971-0.smt2
index 16fdc2b7756fe07b97751f2a784f3f6448a97ba5..254b8c3b3ed9c6951ea72abc4c2fe57f12e0a01a 100644 (file)
--- a/test/regress/regress0/cores/issue4971-0.smt2
+++ b/test/regress/regress0/cores/issue4971-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental -q --check-unsat-cores --cegqi-full
+; COMMAND-LINE: --incremental -q --cegqi-full --produce-unsat-cores
 ; EXPECT: unsat
 ; EXPECT: unsat
 ; EXPECT: (

diff --git a/test/regress/regress0/cores/issue4971-1.smt2 b/test/regress/regress0/cores/issue4971-1.smt2
index 011b7432e5e499226fca688907a1d4eb55950866..fcbd5dbde58d695abbe96a4d22837b1c060e3338 100644 (file)
--- a/test/regress/regress0/cores/issue4971-1.smt2
+++ b/test/regress/regress0/cores/issue4971-1.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --incremental -q --check-unsat-cores
-; COMMAND-LINE: --incremental -q --check-unsat-cores --unsat-cores-mode=sat-proof
+; COMMAND-LINE: --incremental -q --produce-unsat-cores
+; COMMAND-LINE: --incremental -q --unsat-cores-mode=sat-proof --produce-unsat-cores
 ; EXPECT: sat
 ; EXPECT: sat
 (declare-const i2 Int)
@@ -13,4 +13,4 @@
 (assert (< (set.card st9) i11))
 (assert (! (not (<= 5 i5 93 417 i2)) :named IP_46))
 (check-sat)
-(check-sat-assuming ((! (or v6 v6 v6) :named IP_12) (! (or false v6 v6) :named IP_56)))
\ No newline at end of file
+(check-sat-assuming ((! (or v6 v6 v6) :named IP_12) (! (or false v6 v6) :named IP_56)))

diff --git a/test/regress/regress0/cores/issue4971-2.smt2 b/test/regress/regress0/cores/issue4971-2.smt2
index ac9de97d214cbcc55221ec7207d0de40f1f46910..35d6e5d308567b840d7c8aa22dd04c8a083f53c0 100644 (file)
--- a/test/regress/regress0/cores/issue4971-2.smt2
+++ b/test/regress/regress0/cores/issue4971-2.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --incremental --check-unsat-cores
+; COMMAND-LINE: --incremental --produce-unsat-cores
 ; EXPECT: sat
 (set-logic QF_SLIA)
 (assert false)
 (reset-assertions)
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress0/cores/issue4971-3.smt2 b/test/regress/regress0/cores/issue4971-3.smt2
index ebbe07519e20b82b9fe909f126b3d9767095e348..36495b5ede7278a24e797fcc766542388a37162e 100644 (file)
--- a/test/regress/regress0/cores/issue4971-3.smt2
+++ b/test/regress/regress0/cores/issue4971-3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental -q --check-unsat-cores
+; COMMAND-LINE: --incremental -q --produce-unsat-cores
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
@@ -35,4 +35,4 @@
 (check-sat-assuming (IP_2 IP_4))
 (check-sat-assuming (IP_1 IP_3))
 (assert (! (xor v3 v1 v5 v3 v2 (distinct Str19 Str3 Str5 Str9 Str11) (distinct 359 i1) v2 (>= r16 9873987263.0 r9 r0)) :named IP_6))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress0/cores/issue5238.smt2 b/test/regress/regress0/cores/issue5238.smt2
index faf72f0e1d0684bf3f9e18e434608228b76b25bb..765bcdc2cf47b3e37cdd9f30e0f6415e329eea1e 100644 (file)
--- a/test/regress/regress0/cores/issue5238.smt2
+++ b/test/regress/regress0/cores/issue5238.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-check-models
+; COMMAND-LINE: --incremental -q
 ; EXPECT: sat
 ; EXPECT: unsat
 ; EXPECT: unsat

diff --git a/test/regress/regress0/fmf/bug-041417-set-options.cvc.smt2 b/test/regress/regress0/fmf/bug-041417-set-options.cvc.smt2
index 06c1415c2177216626d30c33be7cf4f62c521f66..42c2513f12849281039347f56d261913eae2ae0f 100644 (file)
--- a/test/regress/regress0/fmf/bug-041417-set-options.cvc.smt2
+++ b/test/regress/regress0/fmf/bug-041417-set-options.cvc.smt2
@@ -1,4 +1,5 @@
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :finite-model-find true)

diff --git a/test/regress/regress0/fmf/bug782.smt2 b/test/regress/regress0/fmf/bug782.smt2
index 603c783d3eb38947753f9a8ce1125b231d15f89c..81531b293b4b04aa28aef15e676129531d38d65e 100644 (file)
--- a/test/regress/regress0/fmf/bug782.smt2
+++ b/test/regress/regress0/fmf/bug782.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (set-info :status sat)
 (define-fun $$Bool.isTrue$$ ((b Bool)) Bool b)

diff --git a/test/regress/regress0/fmf/fd-false.smt2 b/test/regress/regress0/fmf/fd-false.smt2
index 20170ea1bf706dca73ff6af9c344f490bc195954..da53e24daa9b5ee7f5504e4b54cbf429ec7d4dc8 100644 (file)
--- a/test/regress/regress0/fmf/fd-false.smt2
+++ b/test/regress/regress0/fmf/fd-false.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (define-fun-rec f ((x Int)) Bool false)
 (assert (not (f 0)))

diff --git a/test/regress/regress0/fmf/issue3661-ccard-dec.smt2 b/test/regress/regress0/fmf/issue3661-ccard-dec.smt2
index 4b120fc9d1f8042528b9410a2bfca06af5530ac5..3f637cd34383557166cfca158d29199001f84dac 100644 (file)
--- a/test/regress/regress0/fmf/issue3661-ccard-dec.smt2
+++ b/test/regress/regress0/fmf/issue3661-ccard-dec.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --fmf-fun -i
 ; EXPECT: sat
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (declare-fun a (Int) Bool)
 (declare-fun b (Int) Bool)

diff --git a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
index 9ee1fa5eb1c2b553bf0fffc4df02eb91b4c0309d..58b00705362f282e00768384899e6b90375248d3 100644 (file)
--- a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
+++ b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --sort-inference --finite-model-find --no-check-unsat-cores
+; COMMAND-LINE: --sort-inference --finite-model-find
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 (set-logic ALL)
 (assert (not (exists ((X Int)) (not (= X 12)) )))
 (check-sat)

diff --git a/test/regress/regress0/fmf/tail_rec.smt2 b/test/regress/regress0/fmf/tail_rec.smt2
index 05ca33aaca3a57b09fd15c3e216c8b703ced53f9..8f9dbd29ed9475787aa6d0a0e40b223b27954162 100644 (file)
--- a/test/regress/regress0/fmf/tail_rec.smt2
+++ b/test/regress/regress0/fmf/tail_rec.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (declare-sort elem 0)
 (declare-datatypes ((list 0)) (((Nil) (Cons (hd elem) (tl list)))))

diff --git a/test/regress/regress0/int-to-bv/basic.smt2 b/test/regress/regress0/int-to-bv/basic.smt2
index 1e30a7ee84190467e5f37eba0bfbcfaf1ff23c46..bf6cc1cb767475a76eca758c1c2a04f6acfb943a 100644 (file)
--- a/test/regress/regress0/int-to-bv/basic.smt2
+++ b/test/regress/regress0/int-to-bv/basic.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=5 --no-check-models
+; COMMAND-LINE: --solve-int-as-bv=5
 (set-logic QF_NIA)
 (declare-const x Int)
 (declare-const y Int)

diff --git a/test/regress/regress0/int-to-bv/neg-consts.smt2 b/test/regress/regress0/int-to-bv/neg-consts.smt2
index 46c08dad59c20512c20ac6ffb6e39bcb24d179b5..0acf5af2e6700ad0123ee7b9b0984e48bd17aa95 100644 (file)
--- a/test/regress/regress0/int-to-bv/neg-consts.smt2
+++ b/test/regress/regress0/int-to-bv/neg-consts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models
+; COMMAND-LINE: --solve-int-as-bv=4
 (set-logic QF_NIA)
 (declare-const x Int)
 (declare-const y Int)

diff --git a/test/regress/regress0/issue5736.smt2 b/test/regress/regress0/issue5736.smt2
index dd4d4f951a5a024c4404058c5405d5ebdd88af73..e0244b419ed7d6b91667a9921b79d16ca38ebb0a 100644 (file)
--- a/test/regress/regress0/issue5736.smt2
+++ b/test/regress/regress0/issue5736.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q --check-unsat-cores --check-models
+; COMMAND-LINE: -q
 (set-info :status sat)
 (declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
 (declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))

diff --git a/test/regress/regress0/issue5743.smt2 b/test/regress/regress0/issue5743.smt2
index b53f0fbefb5c1e19f20c712bded3cc9386bfdcdf..644723916e1026a43b43c4b3992542339eb40945 100644 (file)
--- a/test/regress/regress0/issue5743.smt2
+++ b/test/regress/regress0/issue5743.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --check-models -q
+; COMMAND-LINE: -q
 (set-logic QF_AUFBV)
 (set-info :status sat)
 (declare-fun bv_22-0 () (_ BitVec 1))

diff --git a/test/regress/regress0/issue5947.smt2 b/test/regress/regress0/issue5947.smt2
index 4fbcfb00bce64941d5a019dda44d672b03e516f2..a5c73632385ab8fea7acd0a12fab1fc81e68d90c 100644 (file)
--- a/test/regress/regress0/issue5947.smt2
+++ b/test/regress/regress0/issue5947.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q --check-models
+; COMMAND-LINE: -q
 (set-logic QF_UFBVLIA)
 (set-info :status sat)
 (declare-fun f ((_ BitVec 3)) Int)

diff --git a/test/regress/regress0/issue6741.smt2 b/test/regress/regress0/issue6741.smt2
index 0fbf4edeb3ae17befd6e58d788a31cb3a17b68cc..96f44f9dc40bda1780d8df2adaa7db7cfeacf9d8 100644 (file)
--- a/test/regress/regress0/issue6741.smt2
+++ b/test/regress/regress0/issue6741.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=bitblast --bitblast=eager --check-models
+; COMMAND-LINE: --bv-solver=bitblast --bitblast=eager
 (set-logic QF_BV)
 (set-info :status sat)
 (declare-fun x () (_ BitVec 1))

diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2
index 5724d7fa70c0aa8da6eaec3e0207800b70b66ff2..5ef198120f205d5271d185be8c1fb3c50211858c 100644 (file)
--- a/test/regress/regress0/nl/issue3003.smt2
+++ b/test/regress/regress0/nl/issue3003.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext=none --no-check-models
+; COMMAND-LINE: --nl-ext=none
 ; EXPECT: sat
 ; REQUIRES: poly
 (set-logic QF_NRA)

diff --git a/test/regress/regress0/nl/issue3411.smt2 b/test/regress/regress0/nl/issue3411.smt2
index cef646f16b6c2c9dcba3d3ec054a9aebabfb7676..0aed32dddcd98b6a660b3221ce9ed6bab641aafb 100644 (file)
--- a/test/regress/regress0/nl/issue3411.smt2
+++ b/test/regress/regress0/nl/issue3411.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE: -q
 ; EXPECT: sat
 ; REQUIRES: poly
 (set-logic NRA)

diff --git a/test/regress/regress0/nl/issue3652.smt2 b/test/regress/regress0/nl/issue3652.smt2
index 4b3bdd067203ea8e326c154d41238937f308ae5d..ede4fc368dc1fba73f8da135f01cc87b28dee87b 100644 (file)
--- a/test/regress/regress0/nl/issue3652.smt2
+++ b/test/regress/regress0/nl/issue3652.smt2
@@ -1,4 +1,3 @@
-;COMMAND-LINE: --check-models
 ;REQUIRES: poly
 ;EXPECT: sat
 (set-logic QF_NRA)

diff --git a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2
index 75d4b6e3a86adf178b7dc23f5c8d338a3ae53241..69bb74e849092751b9fdc07b57a18fad37fe55f1 100644 (file)
--- a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2
+++ b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quiet --no-check-models
+; COMMAND-LINE: --quiet
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/issue3991.smt2 b/test/regress/regress0/nl/issue3991.smt2
index c006b288580721783ec52f3933e4a925d1d5a096..c9337beb573517d29302bae52e167f3fb0dbeb86 100644 (file)
--- a/test/regress/regress0/nl/issue3991.smt2
+++ b/test/regress/regress0/nl/issue3991.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --check-unsat-cores
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat

diff --git a/test/regress/regress0/nl/issue5740-2-mod00.smt2 b/test/regress/regress0/nl/issue5740-2-mod00.smt2
index 01930da6d7996c41c0df533074fa2a6a6c0de9c7..f5a462d9ab884194c4c0a6909878b8b776014933 100644 (file)
--- a/test/regress/regress0/nl/issue5740-2-mod00.smt2
+++ b/test/regress/regress0/nl/issue5740-2-mod00.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rewrite-quant --sygus-inst --no-check-models
+; COMMAND-LINE: --ext-rewrite-quant --sygus-inst -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 b/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2
index 69c36179a1f20df1d1044f07d39c1780e7110796..8fd7ec01873929c2c5eb782204bad2e2fe8707c2 100644 (file)
--- a/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2
+++ b/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
+; COMMAND-LINE: --nl-ext-tf-tplanes -q
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (declare-fun x () Real)

diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2
index e7446a8c070fbdb79a1f5aa18d58e88de1b3e1fa..cf4ec5cfb75a298f67943c9b3526cc0d47225490 100644 (file)
--- a/test/regress/regress0/nl/nta/real-pi.smt2
+++ b/test/regress/regress0/nl/nta/real-pi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext=full --no-check-models
+; COMMAND-LINE: --nl-ext=full -q
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
index 96a1d86ba2ab50f5e174d207f28d8e9474228153..ab10a29a54dbd429593f577b3550269e06689be2 100644 (file)
--- a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
+++ b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext-tplanes
 ; REQUIRES: poly
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2
index 217d12cd3412a27073c510d52e56fe569c8957f1..5fac95767b23b4718a5f219d4978b2b70dff7b1e 100644 (file)
--- a/test/regress/regress0/nl/sqrt2-value.smt2
+++ b/test/regress/regress0/nl/sqrt2-value.smt2
@@ -1,5 +1,4 @@
 ; SCRUBBER: sed -e 's/(_ real_algebraic_number.*/(_ real_algebraic_number/'
-; COMMAND-LINE: --no-check-models
 ; REQUIRES: poly
 ; EXPECT: sat
 ; EXPECT: ((x (_ real_algebraic_number

diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2
index a3f64d2b1097a13de036cc0f0bce28d6dd0ee3d9..c1ca4f01553c21f43329d77bcb5dd6a7b473b89b 100644 (file)
--- a/test/regress/regress0/push-pop/bug654-dd.smt2
+++ b/test/regress/regress0/push-pop/bug654-dd.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --incremental --fmf-fun --strings-exp
+; DISABLE-TESTER: model
 (set-logic ALL)
 (declare-datatypes ((List_T_C 0) (T_CustomerType 0)) (
 ((List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C)))

diff --git a/test/regress/regress0/push-pop/issue2137.min.smt2 b/test/regress/regress0/push-pop/issue2137.min.smt2
index 372e8f1f301d95ca2405835902cb2f14521cae09..14d3605d7ea03ef1abb0a1353ac827182eb48fca 100644 (file)
--- a/test/regress/regress0/push-pop/issue2137.min.smt2
+++ b/test/regress/regress0/push-pop/issue2137.min.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --check-unsat-cores
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: unsat
 (set-logic ALL)

diff --git a/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2 b/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2
index f16c6fb901f7313e81395d257eeb6eaba2587eec..6d0adceda7f8bf8ba25c31a22db41b7538669bc4 100644 (file)
--- a/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2
+++ b/test/regress/regress0/push-pop/quant-fun-proc-unfd.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant
+; DISABLE-TESTER: model
 (set-logic UFLIA)
 
 

diff --git a/test/regress/regress0/quantifiers/issue5693-prenex.smt2 b/test/regress/regress0/quantifiers/issue5693-prenex.smt2
index 15ee0e7cf923bc6cd8d0ab80284d4dd7039f1f7e..cc89b78293416a1a7626acb87bc90a40082ab5bd 100644 (file)
--- a/test/regress/regress0/quantifiers/issue5693-prenex.smt2
+++ b/test/regress/regress0/quantifiers/issue5693-prenex.smt2
@@ -1,7 +1,8 @@
-; COMMAND-LINE: --full-saturate-quant -i --no-check-unsat-cores
+; COMMAND-LINE: --full-saturate-quant -i
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 (set-logic ALL)
 (set-option :pre-skolem-quant true)
 (declare-fun v7 () Bool)
 (assert (forall ((q49 Bool) (q55 Bool)) (xor v7 (exists ((q49 Bool)) (xor v7 q49 q49)) v7 (= q55 q49))))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress0/sep/issue3720-check-model.smt2 b/test/regress/regress0/sep/issue3720-check-model.smt2
index 488c558b0db846ac4ce1565d78383f16930fc287..1dac5a805ba5aa8b4d45d659316ace838afedfba 100644 (file)
--- a/test/regress/regress0/sep/issue3720-check-model.smt2
+++ b/test/regress/regress0/sep/issue3720-check-model.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (declare-heap (Int Int))
 (assert sep.emp)

diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 2d35a43d800cc7db88df9253ec7f10211c2411b0..7f811f796cb29e54f5c0725aba69730fbfa4376d 100644 (file)
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_SEP_LIA)
 (declare-heap (Int Int))
 (assert (not sep.emp))

diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2
index 953c5252d768ec001098ef832aa662b1141801b5..0b47edc633996b32535c148aedb78b615e7bc15a 100644 (file)
--- a/test/regress/regress0/sep/nspatial-simp.smt2
+++ b/test/regress/regress0/sep/nspatial-simp.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-fun x () Int)

diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2
index a8039ce5bcebdad407b1151c09764521cf9ec810..49390f937fd0d3bbbdae4ecd15af3c38ae493737 100644 (file)
--- a/test/regress/regress0/sep/simple-080420-const-sets.smt2
+++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-option :produce-models true)
 (set-info :status sat)

diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2
index 1c690cc75e62c56b86e354bb4b27d2dfe1258be5..698fedc769cd5ab5d32692db62ede608cbebc8cf 100644 (file)
--- a/test/regress/regress0/sep/skolem_emp.smt2
+++ b/test/regress/regress0/sep/skolem_emp.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp
+; COMMAND-LINE: --sep-pre-skolem-emp
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (assert (not sep.emp))

diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index d84d900f3f1a5279ebefec50efb63735b1081eaf..eae46e0e5c2d51d95ed23853ac5ec60511bf4caf 100644 (file)
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (assert (wand sep.emp sep.emp))

diff --git a/test/regress/regress0/seq/issue4370-bool-terms.smt2 b/test/regress/regress0/seq/issue4370-bool-terms.smt2
index 8f6a16b458e396cf2ad1a1f2009926365a294984..7d3a7a2d9436edfe2f06fb03c335a5421632a9f9 100644 (file)
--- a/test/regress/regress0/seq/issue4370-bool-terms.smt2
+++ b/test/regress/regress0/seq/issue4370-bool-terms.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-check-models
+; COMMAND-LINE: --strings-exp -q
 (set-logic ALL)
 (set-info :status sat)
 (declare-datatypes ((a 0)) (((b))))

diff --git a/test/regress/regress0/seq/nth-update.smt2 b/test/regress/regress0/seq/nth-update.smt2
index 9ee7e8fa007e7cf10bd496a495f9b4a07ca5a35b..5c194ffad3db9a255d87dfcf2d8084152732d19b 100644 (file)
--- a/test/regress/regress0/seq/nth-update.smt2
+++ b/test/regress/regress0/seq/nth-update.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --seq-array=lazy --no-check-models
+; COMMAND-LINE: --strings-exp --seq-array=lazy -q
 ; EXPECT: sat
 (set-logic QF_SLIA)
 (declare-const x (Seq Int))

diff --git a/test/regress/regress0/seq/rev.smt2 b/test/regress/regress0/seq/rev.smt2
index 071122e4ff4206cbc72877f47b9a833959e38cf7..3297fa83092403ea0f58ea02e2927eccd6560bd4 100644 (file)
--- a/test/regress/regress0/seq/rev.smt2
+++ b/test/regress/regress0/seq/rev.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --seq-array=eager --no-check-unsat-cores
+; COMMAND-LINE: --seq-array=eager
+; DISABLE-TESTER: unsat-core
+; timeout with unsat cores
 (set-logic QF_SLIA)
 (set-info :status unsat)
 

diff --git a/test/regress/regress0/seq/seq-nth.smt2 b/test/regress/regress0/seq/seq-nth.smt2
index ff22a3288bec0a24d09186061079efafb3b98789..af637e2bc75b8dc2fef3bfc0ac8cb60aa58c71c7 100644 (file)
--- a/test/regress/regress0/seq/seq-nth.smt2
+++ b/test/regress/regress0/seq/seq-nth.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-check-models
+; COMMAND-LINE: --strings-exp -q
 ;EXPECT: sat
 (set-logic ALL)
 (declare-fun s () (Seq Int))

diff --git a/test/regress/regress1/bug520.smt2 b/test/regress/regress1/bug520.smt2
index 238fec9141aab22829085a11fcb0a570823f1c19..0422e099cb21e19d63b3b9dc2c6477046abed319 100644 (file)
--- a/test/regress/regress1/bug520.smt2
+++ b/test/regress/regress1/bug520.smt2
@@ -1,7 +1,10 @@
 ; COMMAND-LINE: --bitblast=lazy
-; COMMAND-LINE: --bitblast=eager --no-check-models
+; COMMAND-LINE: --bitblast=eager
 ; COMMAND-LINE: --bv-solver=bitblast-internal
 ; EXPECT: sat
+; DISABLE-TESTER: model
+; Note we disable model testing since the 2nd config is incompatible with models, while the other 2 configurations are.
+; This is not ideal but a limitation of our currently regression infrastructure.
 ; Automatically generated by SBV. Do not edit.
 (set-logic QF_UFBV)
 (set-info :status sat)

diff --git a/test/regress/regress1/bv2int-isabelle.smt2 b/test/regress/regress1/bv2int-isabelle.smt2
index e8d1efe519ec5e090419af302db11bb1364cae76..3a88e75a33a89338aca80ed6f7c4186457f157b4 100644 (file)
--- a/test/regress/regress1/bv2int-isabelle.smt2
+++ b/test/regress/regress1/bv2int-isabelle.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun s$ () (_ BitVec 32))

diff --git a/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
index 9bb1fcb552a7bf13171e50f449b357b14be0eaef..31e4ca4d84205a8e9275adebacbbcbcb47fe8131 100644 (file)
--- a/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
+++ b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --fmf-fun-rlv
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)
 (set-logic ALL)

diff --git a/test/regress/regress1/decision/issue5785.smt2 b/test/regress/regress1/decision/issue5785.smt2
index 1bf48a1b27d42fdab43d8987f53d98eb976dec70..2ae2bccf9b84ae25cc3bae05301f4db6705577b7 100644 (file)
--- a/test/regress/regress1/decision/issue5785.smt2
+++ b/test/regress/regress1/decision/issue5785.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --fmf-fun -i --decision=justification
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALRA)
 (set-option :fmf-fun true)
 (declare-fun v2 () Bool)

diff --git a/test/regress/regress1/fmf-fun-dbu.smt2 b/test/regress/regress1/fmf-fun-dbu.smt2
index b35c98aa955ad5936d7c1dd8959122cef93067e7..ab0490b9bee0004aa0d112beddfee1d01ae64719 100644 (file)
--- a/test/regress/regress1/fmf-fun-dbu.smt2
+++ b/test/regress/regress1/fmf-fun-dbu.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --incremental --fmf-fun --no-check-models
+; COMMAND-LINE: --incremental --fmf-fun
+; DISABLE-TESTER: model
 (set-logic UFDTLIA)
 (set-option :produce-models true)
 (declare-datatypes ((List 0)) (((Nil) (Cons (Cons$head Int) (Cons$tail List)))))

diff --git a/test/regress/regress1/fmf/bug651.smt2 b/test/regress/regress1/fmf/bug651.smt2
index 956a55cd32c33d76455f4aeba2a866478ea6848a..b9734b1e58f0d21148cf7f097f0eabe9ac286ec7 100644 (file)
--- a/test/regress/regress1/fmf/bug651.smt2
+++ b/test/regress/regress1/fmf/bug651.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models --fmf-bound
+; COMMAND-LINE: --fmf-fun --fmf-bound -q
 ; EXPECT: sat
 (set-logic UFDTSLIA)
 (set-option :produce-models true)

diff --git a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2
index 8a853c4b6530cc4e820aa19b5612e01029d06b0a..f5970a741ee75e063cbc0528a666b8eeaa0bd456 100644 (file)
--- a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2
+++ b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --fmf-fun-rlv
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (define-fun $$isTrue$$ ((b Bool)) Bool b)
 (define-fun $$isFalse$$ ((b Bool)) Bool (not b))

diff --git a/test/regress/regress1/fmf/bug764.smt2 b/test/regress/regress1/fmf/bug764.smt2
index cb55d8504bdac98b7d918df539a87776bbd1c63f..5187f4a25b19462036409c2fded2444e5dbe3cd4 100644 (file)
--- a/test/regress/regress1/fmf/bug764.smt2
+++ b/test/regress/regress1/fmf/bug764.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (set-info :status sat)
 

diff --git a/test/regress/regress1/fmf/constr-ground-to.smt2 b/test/regress/regress1/fmf/constr-ground-to.smt2
index dba8a05aec3cb1ac02cdf947fa10e0f05466cd51..395c68382b7489a9f50c6ce2daa5855f1a847d90 100644 (file)
--- a/test/regress/regress1/fmf/constr-ground-to.smt2
+++ b/test/regress/regress1/fmf/constr-ground-to.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic UFDTLIA)
 (declare-datatypes ((Term 0) (IntList 0)) (
        (

diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
index efcae64bcf9f15b3e1a620aab5a117d7bf82981f..0ec2b5c28fc14fef9bde8402af0412d5d483aba4 100644 (file)
--- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
+++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun -q
 ; EXPECT: sat
 (set-logic UFNIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
index 32e9d4178f03a59adc9ac0fce73ca65cdb02234f..35a247689bda4aed9152a0ed9b7f60f754b51dd0 100644 (file)
--- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
+++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun -q
 ; EXPECT: sat
 (set-logic UFNIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/issue916-fmf-or.smt2 b/test/regress/regress1/fmf/issue916-fmf-or.smt2
index 479769188052ce3c4bc9d7933b4a1fc285c4bcbe..33c9329157f7a0c516c1097e478e3b075456b090 100644 (file)
--- a/test/regress/regress1/fmf/issue916-fmf-or.smt2
+++ b/test/regress/regress1/fmf/issue916-fmf-or.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
+; DISABLE-TESTER: model
 
 (set-logic UFDTLIA)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
index 6a8feba5c059cd28dba7f4bf1dbc44e40d26fa75..e7fe960eacbf072aeae2f964256bad458b4e0c54 100644 (file)
--- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-produce-models --ho-elim
+; COMMAND-LINE: --no-produce-models --ho-elim
 ; EXPECT: unsat
 
 (set-logic HO_ALL)

diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
index 3f02e56fd4b6af396b021236741b83d85a3f6c44..e77caa3157091906ba68e77105c6a413d80167ba 100644 (file)
--- a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:  --finite-model-find --no-check-models
+; COMMAND-LINE:  --finite-model-find
 ; EXPECT: sat
 
 (set-logic HO_ALL)

diff --git a/test/regress/regress1/issue3990-sort-inference.smt2 b/test/regress/regress1/issue3990-sort-inference.smt2
index 5d036a84f228eca72b4edb32018dd65d568b0bd3..8cdbddc8a62155d06279dbc582131319439d8241 100644 (file)
--- a/test/regress/regress1/issue3990-sort-inference.smt2
+++ b/test/regress/regress1/issue3990-sort-inference.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --sort-inference --no-check-unsat-cores
+; COMMAND-LINE: --sort-inference
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 (set-logic ABV)
 (set-option :sort-inference true)
 (set-info :status unsat)

diff --git a/test/regress/regress1/model-blocker-values.smt2 b/test/regress/regress1/model-blocker-values.smt2
index b5ab4609b47ef355261e01f44be09b225b9ce6ac..25cb0810c3e5214639fc5e32d6b55b337f07e236 100644 (file)
--- a/test/regress/regress1/model-blocker-values.smt2
+++ b/test/regress/regress1/model-blocker-values.smt2
@@ -1,8 +1,9 @@
-; COMMAND-LINE: --incremental --produce-models --block-models=values --no-check-unsat-cores
+; COMMAND-LINE: --incremental --produce-models --block-models=values
 ; EXPECT: sat
 ; EXPECT: sat
 ; if we only block models restricted to (a,b), then there are only 2 models
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 (set-logic QF_UFLIA)
 (declare-fun a () Int)
 (declare-fun b () Int)

diff --git a/test/regress/regress1/nl/approx-sqrt.smt2 b/test/regress/regress1/nl/approx-sqrt.smt2
index 86e3a6d6f76508f7862b1dbf61b8bfc951b706a7..be2482eb10dd9c591488c4a357aa1549e8454364 100644 (file)
--- a/test/regress/regress1/nl/approx-sqrt.smt2
+++ b/test/regress/regress1/nl/approx-sqrt.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; REQUIRES: poly
 ; EXPECT: sat
 (set-logic QF_NRA)

diff --git a/test/regress/regress1/nl/bug698.smt2 b/test/regress/regress1/nl/bug698.smt2
index 221a5613d1494a4f004dc71a4af7870a7bfc4090..7a969a3b4e061b5dbff7b3e58f7c18a1a87356d5 100644 (file)
--- a/test/regress/regress1/nl/bug698.smt2
+++ b/test/regress/regress1/nl/bug698.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --incremental --nl-ext=full --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --incremental --nl-ext=full --fmf-fun-rlv
+; DISABLE-TESTER: model
 (set-logic UFNIA)
 (set-info :smt-lib-version 2.6)
 

diff --git a/test/regress/regress1/nl/exp-approx.smt2 b/test/regress/regress1/nl/exp-approx.smt2
index f3faceda5a19b8b736107b837b8410319b314fd9..96cf7dc916324cbc07bb7b6bc62caac6638b790e 100644 (file)
--- a/test/regress/regress1/nl/exp-approx.smt2
+++ b/test/regress/regress1/nl/exp-approx.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/exp-soundness-bound.smt2 b/test/regress/regress1/nl/exp-soundness-bound.smt2
index 8074fb2f2bb9094bb262292395d26234fca2d4d8..106b75f3c97ec6e53a1fa8d99e2c06a8676b7fbc 100644 (file)
--- a/test/regress/regress1/nl/exp-soundness-bound.smt2
+++ b/test/regress/regress1/nl/exp-soundness-bound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext=full --decision=internal --no-check-models
+; COMMAND-LINE: --nl-ext=full --decision=internal -q
 ; EXPECT: sat
 (set-logic ALL)
 (assert (or (< 60.3 (exp 4.1) 60.4) (< (exp 5.1) 164.1)))

diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
index 3a4a23dbb3bc1bd2175f25f52b3d4a1c5a58b0ff..fa9616847097602c2b6cbeaf53470441836eff27 100644 (file)
--- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
+++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
@@ -1,5 +1,5 @@
 ; SCRUBBER: sed -e 's/((x (_ real_algebraic_number .*/((x (_ real_algebraic_number/'
-; COMMAND-LINE: --produce-models --no-check-models
+; COMMAND-LINE: --produce-models
 ; REQUIRES: poly
 ; EXPECT: sat
 ; EXPECT: ((x (_ real_algebraic_number

diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2
index f863842def025462c35d2fd755f21963324f4054..8af32cde1a71ebb61ea481cef88ec8edf8d817f2 100644 (file)
--- a/test/regress/regress1/nl/issue3647.smt2
+++ b/test/regress/regress1/nl/issue3647.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always
+; COMMAND-LINE: --produce-models --decision=internal --nl-rlv=always -q
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/issue4791-llr.smt2 b/test/regress/regress1/nl/issue4791-llr.smt2
index d29a16313ac7c3b0ddd009f4dadb5195b39bfc86..30a6554c1213544ea71f3fd74fd546774f538e8b 100644 (file)
--- a/test/regress/regress1/nl/issue4791-llr.smt2
+++ b/test/regress/regress1/nl/issue4791-llr.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --learned-rewrite --no-check-unsat-cores
+; COMMAND-LINE: --learned-rewrite
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 ;
 ;!(a,b,c).( 0<=b & 1<=c & 0<=a & 1<=c
 ;               =>

diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2
index 4fb0732a375e352a718a1a98e85466a63e4de4a8..267a012cf10c66237b625bfc3da20c44a3a70a84 100644 (file)
--- a/test/regress/regress1/nl/sin1-deq-sat.smt2
+++ b/test/regress/regress1/nl/sin1-deq-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always
+; COMMAND-LINE: --nl-ext-tf-tplanes --nl-rlv=always -q
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2
index 9c1d9cef67ef53f92f0f706093acd304a9f2e478..cf8dd7f91b5cbf0e4d222a7f300f86e978022d49 100644 (file)
--- a/test/regress/regress1/nl/sin1-sat.smt2
+++ b/test/regress/regress1/nl/sin1-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always
+; COMMAND-LINE: --nl-ext-tf-tplanes --nl-rlv=always -q
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2 b/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2
index fde3b9a81ffacb7c6d90661ac2ff207b35b22d1a..e08d1607a0f76cfdbbcc0607c36eedf39f615dfa 100644 (file)
--- a/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2
+++ b/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; REQUIRES: poly
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress1/push-pop/quant-fun-proc-unmacro.smt2 b/test/regress/regress1/push-pop/quant-fun-proc-unmacro.smt2
index 7cacfca98bfbb4e3b803ddc2ec7865b49a3479a3..20dcc2931538841a8df72237ea0f89bd7b64c82f 100644 (file)
--- a/test/regress/regress1/push-pop/quant-fun-proc-unmacro.smt2
+++ b/test/regress/regress1/push-pop/quant-fun-proc-unmacro.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant
+; DISABLE-TESTER: model
 (set-logic UFLIA)
 
 

diff --git a/test/regress/regress1/push-pop/quant-fun-proc.smt2 b/test/regress/regress1/push-pop/quant-fun-proc.smt2
index 2b5c6cab9096e6c6636e0ce1b3acdcaf831822dc..472168f0058cf98ef5f5cf39d287fa8a016b3c3c 100644 (file)
--- a/test/regress/regress1/push-pop/quant-fun-proc.smt2
+++ b/test/regress/regress1/push-pop/quant-fun-proc.smt2
@@ -1,4 +1,7 @@
-; COMMAND-LINE: --incremental --fmf-fun --macros-quant --macros-quant-mode=ground --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --incremental --fmf-fun --macros-quant --macros-quant-mode=ground
+; DISABLE-TESTER: model
+; DISABLE-TESTER: unsat-core
+; unknowns when testing unsat cores
 (set-logic UFLIA)
 
 (define-fun f ((x Int)) Int x)

diff --git a/test/regress/regress1/quantifiers/issue3316.smt2 b/test/regress/regress1/quantifiers/issue3316.smt2
index 2fc38f4b47d59229000c792c5aa963bd3b060661..e4bdcda04d1a4acd6e23c01e0fe5e189f609109d 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3316.smt2
+++ b/test/regress/regress1/quantifiers/issue3316.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --fmf-fun-rlv
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)
 (set-logic ALL)

diff --git a/test/regress/regress1/quantifiers/issue3317.smt2 b/test/regress/regress1/quantifiers/issue3317.smt2
index 758878af2011e5b2e0e32008ffba1e9fe5c824da..0df91e9d2670dfc973c3c90950d80c66d9ef4851 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3317.smt2
+++ b/test/regress/regress1/quantifiers/issue3317.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --fmf-fun-rlv
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)
 (set-logic ALL)

diff --git a/test/regress/regress1/quantifiers/issue3628.smt2 b/test/regress/regress1/quantifiers/issue3628.smt2
index 9843b92ffaa6d0797cf3917c1ab1017318f1e851..f4831fd6f460fb658b878b7c3853622e4261f690 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3628.smt2
+++ b/test/regress/regress1/quantifiers/issue3628.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic NIRA)
 (declare-fun a () Real)

diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2
index e1a923f9845e30e393919fe72534df4ac797c4b4..ebb89a4c93e4ab9f968fa635086bf5a17ede0a3b 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3664.smt2
+++ b/test/regress/regress1/quantifiers/issue3664.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --fmf-fun-rlv --sygus-inference --no-check-models
+; COMMAND-LINE: --fmf-fun-rlv --sygus-inference
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_NRA)
 (declare-fun a () Real)
 (assert (= (/ a a) 1.0))

diff --git a/test/regress/regress1/quantifiers/issue3765.smt2 b/test/regress/regress1/quantifiers/issue3765.smt2
index 4947586f21f4d57e9a6ec8162d46e3dc339521e9..dedb43a4804b8c2621223dde962da82f3c77661b 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3765.smt2
+++ b/test/regress/regress1/quantifiers/issue3765.smt2
@@ -1,17 +1,17 @@
-; COMMAND-LINE: --fmf-fun --no-check-models\r
-; EXPECT: sat\r
-\r
-(set-info :smt-lib-version 2.6)\r
-(set-option :produce-models true)\r
-(set-logic ALL)\r
-(define-funs-rec (\r
-(f11((va9 Int))Int)\r
-(f3((v1f Int))Int)\r
-)\r
-( (f3 (ite (= 0 va9) (- 1) (div (- 1) va9)))\r
- (- (ite (= 0 v1f) 0 (mod 0 v1f))) \r
-))\r
-(declare-fun v18d() Int)\r
-(assert (= 0 (f11 v18d)))\r
-(assert (= 22 v18d))\r
-(check-sat)\r
+; COMMAND-LINE: --fmf-fun -q
+; EXPECT: sat
+
+(set-info :smt-lib-version 2.6)
+(set-option :produce-models true)
+(set-logic ALL)
+(define-funs-rec (
+(f11((va9 Int))Int)
+(f3((v1f Int))Int)
+)
+( (f3 (ite (= 0 va9) (- 1) (div (- 1) va9)))
+ (- (ite (= 0 v1f) 0 (mod 0 v1f))) 
+))
+(declare-fun v18d() Int)
+(assert (= 0 (f11 v18d)))
+(assert (= 22 v18d))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
index f3a3c99b75b81d04029f44900473167c119751cb..46bd7a17876e0c2f030100fbf3156a1bc86de4ff 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
+++ b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rewrite-quant --no-check-models
+; COMMAND-LINE: --ext-rewrite-quant -q
 ; EXPECT: sat
 (set-logic NIA)
 (assert (exists ((x Int)) (= (div 1 x x) x)))

diff --git a/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2 b/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
index fa9691578d047157fd4e86cca343715808b72c91..3fe54e2c6000aff0caae707a96537fb17d271bae 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
+++ b/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inst --no-check-models
+; COMMAND-LINE: --sygus-inst -q
 ; EXPECT: sat
 (set-logic NIRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/issue5469-aext.smt2 b/test/regress/regress1/quantifiers/issue5469-aext.smt2
index d66afb91a619b17e123a92e9ea9a1df636a979d3..3549a770f84452437de102ec7b4375baa62c7b6f 100644 (file)
--- a/test/regress/regress1/quantifiers/issue5469-aext.smt2
+++ b/test/regress/regress1/quantifiers/issue5469-aext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inst --strings-exp --no-check-models
+; COMMAND-LINE: --sygus-inst --strings-exp -q
 ; EXPECT: sat
 (set-logic NIA)
 (set-option :sygus-inst true)

diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
index 0cd319ffbb5397aad8847b32cef8215ecb912b39..e605008339674ef234d9a3f9df0a135df85d32cc 100644 (file)
--- a/test/regress/regress1/quantifiers/issue5470-aext.smt2
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic NIA)
 (set-option :strings-exp true)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 b/test/regress/regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
index 9ccde98cd10d4dd91ad5b1ecad19c4ba6a2279aa..64e0c05291c04f93980f3db55cfc9147276b5ffe 100644 (file)
--- a/test/regress/regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
+++ b/test/regress/regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inst --no-check-models
+; COMMAND-LINE: --sygus-inst -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2
index b428cc52a06c706f396b7575c745986aa1911210..30cb757c2fcadefc3af579fc35eaf4da9111db6e 100644 (file)
--- a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2
+++ b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-models
 ; REQUIRES: poly
 (set-logic NRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2
index b7cc50885757b6ec82a40ad5405ec9c19b9eecdc..6ef920613b54ae322455225b4d04cefb120d9d41 100644 (file)
--- a/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2
+++ b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inst --no-check-models
+; COMMAND-LINE: --sygus-inst -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun b (Int) Int)

diff --git a/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2
index 39b92a6ad39553692d5a091eb70076cfd882cb60..13c675609bfdd23c27f8d8397604ea599c8201c6 100644 (file)
--- a/test/regress/regress1/quantifiers/issue6775-vts-int.smt2
+++ b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -i --no-check-models
+; COMMAND-LINE: -i
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic NIA)

diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
index 55338bf6c95e91f5d183e4807d00081130d3fefc..9b2d1161e7563b2b2a60425ff505a137a3263b33 100644 (file)
--- a/test/regress/regress1/quantifiers/qid-debug-inst.smt2
+++ b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
@@ -1,9 +1,9 @@
 ; REQUIRES: no-competition
-; COMMAND-LINE: -o inst --no-check-unsat-cores
+; COMMAND-LINE: -o inst
 ; EXPECT: (num-instantiations myQuant1 1)
 ; EXPECT: (num-instantiations myQuant2 1)
 ; EXPECT: unsat
-
+; DISABLE-TESTER: unsat-core
 (set-logic UFLIA)
 (declare-fun P (Int) Bool)
 (declare-fun R (Int) Bool)

diff --git a/test/regress/regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 b/test/regress/regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
index fc22a8af880cd0949cd04ec8c83238ae08862483..e7be953ceb7dc41b6645de89b32a01edfa69e43c 100644 (file)
--- a/test/regress/regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
+++ b/test/regress/regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --full-saturate-quant --multi-trigger-cache --no-check-unsat-cores
+; COMMAND-LINE: --full-saturate-quant --multi-trigger-cache
 ; EXPECT: unsat
 (set-logic AUFLIRA)
 (set-info :status unsat)

diff --git a/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 b/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
index 39790c38dff42503846344e1aa2df056dc52165b..10aefca49c54e42ad2edff2a069df0607c9787cf 100644 (file)
--- a/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
+++ b/test/regress/regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inst --no-check-models
+; COMMAND-LINE: --sygus-inst
 (set-info :smt-lib-version 2.6)
 (set-logic UFNIA)
 (set-info :source |

diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 465408cc51c648ba6dff16da3bfcfa5a015a4a79..fee3033302e5b66511cf6023039b673e2961034c 100644 (file)
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 
 ; Note we require disabling proofs/unsat cores due to timeouts in nightlies
 

diff --git a/test/regress/regress1/sep/crash1220.smt2 b/test/regress/regress1/sep/crash1220.smt2
index 241f69b770b797f6c45d3c32a7955496f01616d8..c839525626ef5a870a1ae5c8f83f98011db13609 100644 (file)
--- a/test/regress/regress1/sep/crash1220.smt2
+++ b/test/regress/regress1/sep/crash1220.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2
index e9915bf4b7ad391b4469e115891070188c48a085..f50f9301f823ba57a5bbd9fa927b7958c097ef34 100644 (file)
--- a/test/regress/regress1/sep/dispose-list-4-init.smt2
+++ b/test/regress/regress1/sep/dispose-list-4-init.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 
 (declare-sort Loc 0)

diff --git a/test/regress/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2
index c40106c48a45712dfe8ff2c951dda86d11815c84..f1e81d38e7fc796101ada395d4bbc9ed41eb9560 100644 (file)
--- a/test/regress/regress1/sep/fmf-nemp-2.smt2
+++ b/test/regress/regress1/sep/fmf-nemp-2.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --finite-model-find --no-check-models
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic ALL)
 (declare-sort U 0)
 (declare-heap (U Int))

diff --git a/test/regress/regress1/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2
index c6d239ec0515aba2653c84696475286991bd8ee7..d12e9d6389bd6c387f439baa7064dee74e3fa6ef 100644 (file)
--- a/test/regress/regress1/sep/loop-1220.smt2
+++ b/test/regress/regress1/sep/loop-1220.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/sep-neg-1refine.smt2 b/test/regress/regress1/sep/sep-neg-1refine.smt2
index 867d4ccb8650dab852eb183a7b3f00c929e24a28..6e281fb66525955a3983f076deeb7a56aab56140 100644 (file)
--- a/test/regress/regress1/sep/sep-neg-1refine.smt2
+++ b/test/regress/regress1/sep/sep-neg-1refine.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 b/test/regress/regress1/sep/sep-neg-nstrict2.smt2
index e66a39f23977c791787fc926765a7fe365071fe2..7f11186fe2faeb8dff41ed66be6fb0745cede32f 100644 (file)
--- a/test/regress/regress1/sep/sep-neg-nstrict2.smt2
+++ b/test/regress/regress1/sep/sep-neg-nstrict2.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/sep-neg-simple.smt2 b/test/regress/regress1/sep/sep-neg-simple.smt2
index dc114b0dd0b62e2dc0c05c6cd96b5bca2c97a39d..ca718df1b72f2a7e3c2d0a01ea32ef6aa71245c7 100644 (file)
--- a/test/regress/regress1/sep/sep-neg-simple.smt2
+++ b/test/regress/regress1/sep/sep-neg-simple.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/sep-neg-swap.smt2 b/test/regress/regress1/sep/sep-neg-swap.smt2
index b34e6031f28fb916288ba7e86311f5bfd165f5e6..8a47fc7f7bff1f55f948b1758ff485cb8af69b14 100644 (file)
--- a/test/regress/regress1/sep/sep-neg-swap.smt2
+++ b/test/regress/regress1/sep/sep-neg-swap.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/sep-nterm-again.smt2 b/test/regress/regress1/sep/sep-nterm-again.smt2
index 0b38bd1890f22f43f3b4e72185df80cb0636806e..b3fbf7e1091708d9399a8960beb6e61eb9a28a29 100644 (file)
--- a/test/regress/regress1/sep/sep-nterm-again.smt2
+++ b/test/regress/regress1/sep/sep-nterm-again.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2
index eee6fa2118bc41d434a8248e231801df28f345ec..e6aefc6989c0303c09ecbc42b210ce9f026c4a2a 100644 (file)
--- a/test/regress/regress1/sep/sep-simp-unc.smt2
+++ b/test/regress/regress1/sep/sep-simp-unc.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-sort U 0)

diff --git a/test/regress/regress1/sep/simple-neg-sat.smt2 b/test/regress/regress1/sep/simple-neg-sat.smt2
index 612776cfa8372dfadbe8d8b11d5a5f983232fd2f..6b8c771ac03993b60702bbe90ffd3912431a648f 100644 (file)
--- a/test/regress/regress1/sep/simple-neg-sat.smt2
+++ b/test/regress/regress1/sep/simple-neg-sat.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2
index 334908e64d43507d15a3d4b805f8de081b883c1e..999a0806075071da012a1f338cc51ca0989ba185 100644 (file)
--- a/test/regress/regress1/sep/wand-0526-sat.smt2
+++ b/test/regress/regress1/sep/wand-0526-sat.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (declare-fun x () Int)

diff --git a/test/regress/regress1/sep/wand-false.smt2 b/test/regress/regress1/sep/wand-false.smt2
index 3d496782c1c979c1f97899b779dc6b8c8e1806d3..69bd9fcf5f3b7767e7fee60436800625e427a723 100644 (file)
--- a/test/regress/regress1/sep/wand-false.smt2
+++ b/test/regress/regress1/sep/wand-false.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2
index 4239a415eaf97b49fd4b2e410b380dcab7d4a28f..ecd842766cf468745b776d8b0274501b48facb9f 100644 (file)
--- a/test/regress/regress1/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (declare-fun x () Int)

diff --git a/test/regress/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2
index 15362f227cb80b7a21c4170276d869e48e52f25c..8db329e9236225339b23be449c5dceccd3a0fa46 100644 (file)
--- a/test/regress/regress1/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/sep/wand-simp-sat.smt2 b/test/regress/regress1/sep/wand-simp-sat.smt2
index 79c12c02892ad07993f4124d68d5dbc7be224e45..91782600ec27aee9ef82bdca09c22c1dc699de97 100644 (file)
--- a/test/regress/regress1/sep/wand-simp-sat.smt2
+++ b/test/regress/regress1/sep/wand-simp-sat.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (declare-heap (Int Int))
 (declare-fun x () Int)

diff --git a/test/regress/regress1/sep/wand-simp-sat2.smt2 b/test/regress/regress1/sep/wand-simp-sat2.smt2
index 76aed570f195ccc49fffbc8838b4edf7c1ea67bb..cdb69d95b630c60b8a90a1b91ab9ee527422c57b 100644 (file)
--- a/test/regress/regress1/sep/wand-simp-sat2.smt2
+++ b/test/regress/regress1/sep/wand-simp-sat2.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
+; DISABLE-TESTER: model
 (set-logic QF_ALL)
 (set-info :status sat)
 (declare-heap (Int Int))

diff --git a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2 b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
index 0fc0e8b53594864dfd1432506f723be496fc8c60..ec948d55a47d240349734e5c6989b3aa930a1945 100644 (file)
--- a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
+++ b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
@@ -1,261 +1,262 @@
-; COMMAND-LINE: --strings-exp --fmf-fun-rlv -i --no-check-models\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-; EXPECT: sat\r
-\r
-; note that fmf-fun-rlv is incompatible with check-models\r
-\r
-(set-info :smt-lib-version 2.6)\r
-(set-option :produce-models true)\r
-(set-logic ALL)\r
-(declare-datatypes ((a0 0)(a1 0)(a2 0)) (((c0$0) (c0$1) (c0$2) (c0$3 (c0$3$0 a1) (c0$3$1 Int) (c0$3$2 String) (c0$3$3 Int)) (c0$4 (c0$4$0 Int)) (c0$5))((c1$0 (c1$0$0 a0) (c1$0$1 a0) (c1$0$2 String) (c1$0$3 Int)) (c1$1 (c1$1$0 Int)) (c1$2) (c1$3 (c1$3$0 Int)) (c1$4) (c1$5))((c2$0 (c2$0$0 Int) (c2$0$1 a0)) (c2$1 (c2$1$0 String) (c2$1$1 a0) (c2$1$2 a1)))))\r
-(push 1)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v0() a0)\r
-(declare-fun v1() a2)\r
-(declare-fun v2() a2)\r
-(declare-fun v3() a0)\r
-(declare-fun v4() Bool)\r
-(declare-fun v5() a1)\r
-(declare-fun v6() Bool)\r
-(declare-fun v7() String)\r
-(declare-fun v8() a2)\r
-(pop 1)\r
-(push 1)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v9() a2)\r
-(declare-fun va() a1)\r
-(declare-fun vb() Int)\r
-(declare-fun vc() Bool)\r
-(declare-fun vd() Int)\r
-(declare-fun ve() Bool)\r
-(declare-fun vf() Bool)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v10() a1)\r
-(declare-fun v11() a0)\r
-(declare-fun v12() a1)\r
-(declare-fun v13() Int)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v14() Bool)\r
-(declare-fun v15() a0)\r
-(declare-fun v16() Bool)\r
-(declare-fun v17() a1)\r
-(declare-fun v18() a2)\r
-(declare-fun v19() a0)\r
-(declare-fun v1a() Int)\r
-(declare-fun v1b() Bool)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v1c() String)\r
-(declare-fun v1d() Int)\r
-(declare-fun v1e() a1)\r
-(declare-fun v1f() a0)\r
-(declare-fun v20() Bool)\r
-(declare-fun v21() Int)\r
-(declare-fun v22() Int)\r
-(declare-fun v23() String)\r
-(declare-fun v24() a0)\r
-(declare-fun v25() a0)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v26() Bool)\r
-(declare-fun v27() Bool)\r
-(declare-fun v28() Int)\r
-(declare-fun v29() a2)\r
-(declare-fun v2a() Int)\r
-(declare-fun v2b() Int)\r
-(declare-fun v2c() String)\r
-(declare-fun v2d() String)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v2e() a2)\r
-(declare-fun v2f() a1)\r
-(declare-fun v30() a0)\r
-(declare-fun v31() a2)\r
-(declare-fun v32() String)\r
-(declare-fun v33() Bool)\r
-(declare-fun v34() Int)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v35() String)\r
-(declare-fun v36() a1)\r
-(declare-fun v37() a1)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v38() a2)\r
-(declare-fun v39() Bool)\r
-(pop 1)\r
-(define-funs-rec ((fa((v38 a2)(v39 Bool))a2)(f9((v35 String)(v36 a1)(v37 a1))String)(f8((v2e a2)(v2f a1)(v30 a0)(v31 a2)(v32 String)(v33 Bool)(v34 Int))a0)(f7((v26 Bool)(v27 Bool)(v28 Int)(v29 a2)(v2a Int)(v2b Int)(v2c String)(v2d String))a0)(f6((v1c String)(v1d Int)(v1e a1)(v1f a0)(v20 Bool)(v21 Int)(v22 Int)(v23 String)(v24 a0)(v25 a0))Int)(f5((v14 Bool)(v15 a0)(v16 Bool)(v17 a1)(v18 a2)(v19 a0)(v1a Int)(v1b Bool))a0)(f4((v10 a1)(v11 a0)(v12 a1)(v13 Int))Bool)(f3((v9 a2)(va a1)(vb Int)(vc Bool)(vd Int)(ve Bool)(vf Bool))Int)(f2()Int)(f1((v0 a0)(v1 a2)(v2 a2)(v3 a0)(v4 Bool)(v5 a1)(v6 Bool)(v7 String)(v8 a2))Int)(f0()Bool))(v38 "\xea" (c0$3 c1$5 1 "\xc6\xff" (- 2)) c0$5 (- 9) (c0$3 c1$4 0 "" v1a) (str.< (ite (is-c0$4 v11) "\xe8" "") "\x19") 0 (- 1) 0 false))\r
-(push 1)\r
-(assert true)\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v3a() a0)\r
-(declare-fun v3b() a2)\r
-(declare-fun v3c() a2)\r
-(declare-fun v3d() a0)\r
-(declare-fun v3e() Bool)\r
-(declare-fun v3f() a1)\r
-(declare-fun v40() Bool)\r
-(declare-fun v41() String)\r
-(declare-fun v42() a2)\r
-(assert true)\r
-(assert (= (c0$4 0) v3a))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v3b))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v3c))\r
-(assert (= (c0$4 0) v3d))\r
-(assert v3e)\r
-(assert (= c1$2 v3f))\r
-(assert v40)\r
-(assert (= "\xc4\xbf)9N\xc2]" v41))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v42))\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(assert true)\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v43() a2)\r
-(declare-fun v44() a1)\r
-(declare-fun v45() Int)\r
-(declare-fun v46() Bool)\r
-(declare-fun v47() Int)\r
-(declare-fun v48() Bool)\r
-(declare-fun v49() Bool)\r
-(assert true)\r
-(assert (= (c2$1 ";," c0$0 c1$4) v43))\r
-(assert (= c1$2 v44))\r
-(assert (= 9 v45))\r
-(assert v46)\r
-(assert (= 9 v47))\r
-(assert v48)\r
-(assert v49)\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v4a() a1)\r
-(declare-fun v4b() a0)\r
-(declare-fun v4c() a1)\r
-(declare-fun v4d() Int)\r
-(assert (not (f4 v4a v4b v4c v4d)))\r
-(assert (= c1$2 v4a))\r
-(assert (= (c0$4 0) v4b))\r
-(assert (= c1$2 v4c))\r
-(assert (= 9 v4d))\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v4e() Bool)\r
-(declare-fun v4f() a0)\r
-(declare-fun v50() Bool)\r
-(declare-fun v51() a1)\r
-(declare-fun v52() a2)\r
-(declare-fun v53() a0)\r
-(declare-fun v54() Int)\r
-(declare-fun v55() Bool)\r
-(assert (= (c0$3 c1$4 0 "" 9) (f5 v4e v4f v50 v51 v52 v53 v54 v55)))\r
-(assert v4e)\r
-(assert (= (c0$4 0) v4f))\r
-(assert v50)\r
-(assert (= c1$2 v51))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v52))\r
-(assert (= (c0$4 0) v53))\r
-(assert (= 9 v54))\r
-(assert v55)\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v56() String)\r
-(declare-fun v57() Int)\r
-(declare-fun v58() a1)\r
-(declare-fun v59() a0)\r
-(declare-fun v5a() Bool)\r
-(declare-fun v5b() Int)\r
-(declare-fun v5c() Int)\r
-(declare-fun v5d() String)\r
-(declare-fun v5e() a0)\r
-(declare-fun v5f() a0)\r
-(assert true)\r
-(assert (= "\xc4\xbf)9N\xc2]" v56))\r
-(assert (= 9 v57))\r
-(assert (= c1$2 v58))\r
-(assert (= (c0$4 0) v59))\r
-(assert v5a)\r
-(assert (= 9 v5b))\r
-(assert (= 9 v5c))\r
-(assert (= "\xc4\xbf)9N\xc2]" v5d))\r
-(assert (= (c0$4 0) v5e))\r
-(assert (= (c0$4 0) v5f))\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v60() Bool)\r
-(declare-fun v61() Bool)\r
-(declare-fun v62() Int)\r
-(declare-fun v63() a2)\r
-(declare-fun v64() Int)\r
-(declare-fun v65() Int)\r
-(declare-fun v66() String)\r
-(declare-fun v67() String)\r
-(assert true)\r
-(assert v60)\r
-(assert v61)\r
-(assert (= 9 v62))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v63))\r
-(assert (= 9 v64))\r
-(assert (= 9 v65))\r
-(assert (= "\xc4\xbf)9N\xc2]" v66))\r
-(assert (= "\xc4\xbf)9N\xc2]" v67))\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v68() a2)\r
-(declare-fun v69() a1)\r
-(declare-fun v6a() a0)\r
-(declare-fun v6b() a2)\r
-(declare-fun v6c() String)\r
-(declare-fun v6d() Bool)\r
-(declare-fun v6e() Int)\r
-(assert true)\r
-(assert (= (c2$1 ";," c0$0 c1$4) v68))\r
-(assert (= c1$2 v69))\r
-(assert (= (c0$4 0) v6a))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v6b))\r
-(assert (= "\xc4\xbf)9N\xc2]" v6c))\r
-(assert v6d)\r
-(assert (= 9 v6e))\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v6f() String)\r
-(declare-fun v70() a1)\r
-(declare-fun v71() a1)\r
-(assert true)\r
-(assert (= "\xc4\xbf)9N\xc2]" v6f))\r
-(assert (= c1$2 v70))\r
-(assert (= c1$2 v71))\r
-(check-sat)\r
-(pop 1)\r
-(push 1)\r
-(declare-fun v72() a2)\r
-(declare-fun v73() Bool)\r
-(assert (= (c2$1 ";," c0$0 c1$4) (fa v72 v73)))\r
-(assert (= (c2$1 ";," c0$0 c1$4) v72))\r
-(assert v73)\r
-(check-sat)\r
-(pop 1)\r
-(exit)\r
+; COMMAND-LINE: --strings-exp --fmf-fun-rlv -i
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; DISABLE-TESTER: model
+
+; note that fmf-fun-rlv is incompatible with check-models
+
+(set-info :smt-lib-version 2.6)
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes ((a0 0)(a1 0)(a2 0)) (((c0$0) (c0$1) (c0$2) (c0$3 (c0$3$0 a1) (c0$3$1 Int) (c0$3$2 String) (c0$3$3 Int)) (c0$4 (c0$4$0 Int)) (c0$5))((c1$0 (c1$0$0 a0) (c1$0$1 a0) (c1$0$2 String) (c1$0$3 Int)) (c1$1 (c1$1$0 Int)) (c1$2) (c1$3 (c1$3$0 Int)) (c1$4) (c1$5))((c2$0 (c2$0$0 Int) (c2$0$1 a0)) (c2$1 (c2$1$0 String) (c2$1$1 a0) (c2$1$2 a1)))))
+(push 1)
+(pop 1)
+(push 1)
+(declare-fun v0() a0)
+(declare-fun v1() a2)
+(declare-fun v2() a2)
+(declare-fun v3() a0)
+(declare-fun v4() Bool)
+(declare-fun v5() a1)
+(declare-fun v6() Bool)
+(declare-fun v7() String)
+(declare-fun v8() a2)
+(pop 1)
+(push 1)
+(pop 1)
+(push 1)
+(declare-fun v9() a2)
+(declare-fun va() a1)
+(declare-fun vb() Int)
+(declare-fun vc() Bool)
+(declare-fun vd() Int)
+(declare-fun ve() Bool)
+(declare-fun vf() Bool)
+(pop 1)
+(push 1)
+(declare-fun v10() a1)
+(declare-fun v11() a0)
+(declare-fun v12() a1)
+(declare-fun v13() Int)
+(pop 1)
+(push 1)
+(declare-fun v14() Bool)
+(declare-fun v15() a0)
+(declare-fun v16() Bool)
+(declare-fun v17() a1)
+(declare-fun v18() a2)
+(declare-fun v19() a0)
+(declare-fun v1a() Int)
+(declare-fun v1b() Bool)
+(pop 1)
+(push 1)
+(declare-fun v1c() String)
+(declare-fun v1d() Int)
+(declare-fun v1e() a1)
+(declare-fun v1f() a0)
+(declare-fun v20() Bool)
+(declare-fun v21() Int)
+(declare-fun v22() Int)
+(declare-fun v23() String)
+(declare-fun v24() a0)
+(declare-fun v25() a0)
+(pop 1)
+(push 1)
+(declare-fun v26() Bool)
+(declare-fun v27() Bool)
+(declare-fun v28() Int)
+(declare-fun v29() a2)
+(declare-fun v2a() Int)
+(declare-fun v2b() Int)
+(declare-fun v2c() String)
+(declare-fun v2d() String)
+(pop 1)
+(push 1)
+(declare-fun v2e() a2)
+(declare-fun v2f() a1)
+(declare-fun v30() a0)
+(declare-fun v31() a2)
+(declare-fun v32() String)
+(declare-fun v33() Bool)
+(declare-fun v34() Int)
+(pop 1)
+(push 1)
+(declare-fun v35() String)
+(declare-fun v36() a1)
+(declare-fun v37() a1)
+(pop 1)
+(push 1)
+(declare-fun v38() a2)
+(declare-fun v39() Bool)
+(pop 1)
+(define-funs-rec ((fa((v38 a2)(v39 Bool))a2)(f9((v35 String)(v36 a1)(v37 a1))String)(f8((v2e a2)(v2f a1)(v30 a0)(v31 a2)(v32 String)(v33 Bool)(v34 Int))a0)(f7((v26 Bool)(v27 Bool)(v28 Int)(v29 a2)(v2a Int)(v2b Int)(v2c String)(v2d String))a0)(f6((v1c String)(v1d Int)(v1e a1)(v1f a0)(v20 Bool)(v21 Int)(v22 Int)(v23 String)(v24 a0)(v25 a0))Int)(f5((v14 Bool)(v15 a0)(v16 Bool)(v17 a1)(v18 a2)(v19 a0)(v1a Int)(v1b Bool))a0)(f4((v10 a1)(v11 a0)(v12 a1)(v13 Int))Bool)(f3((v9 a2)(va a1)(vb Int)(vc Bool)(vd Int)(ve Bool)(vf Bool))Int)(f2()Int)(f1((v0 a0)(v1 a2)(v2 a2)(v3 a0)(v4 Bool)(v5 a1)(v6 Bool)(v7 String)(v8 a2))Int)(f0()Bool))(v38 "\xea" (c0$3 c1$5 1 "\xc6\xff" (- 2)) c0$5 (- 9) (c0$3 c1$4 0 "" v1a) (str.< (ite (is-c0$4 v11) "\xe8" "") "\x19") 0 (- 1) 0 false))
+(push 1)
+(assert true)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v3a() a0)
+(declare-fun v3b() a2)
+(declare-fun v3c() a2)
+(declare-fun v3d() a0)
+(declare-fun v3e() Bool)
+(declare-fun v3f() a1)
+(declare-fun v40() Bool)
+(declare-fun v41() String)
+(declare-fun v42() a2)
+(assert true)
+(assert (= (c0$4 0) v3a))
+(assert (= (c2$1 ";," c0$0 c1$4) v3b))
+(assert (= (c2$1 ";," c0$0 c1$4) v3c))
+(assert (= (c0$4 0) v3d))
+(assert v3e)
+(assert (= c1$2 v3f))
+(assert v40)
+(assert (= "\xc4\xbf)9N\xc2]" v41))
+(assert (= (c2$1 ";," c0$0 c1$4) v42))
+(check-sat)
+(pop 1)
+(push 1)
+(assert true)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v43() a2)
+(declare-fun v44() a1)
+(declare-fun v45() Int)
+(declare-fun v46() Bool)
+(declare-fun v47() Int)
+(declare-fun v48() Bool)
+(declare-fun v49() Bool)
+(assert true)
+(assert (= (c2$1 ";," c0$0 c1$4) v43))
+(assert (= c1$2 v44))
+(assert (= 9 v45))
+(assert v46)
+(assert (= 9 v47))
+(assert v48)
+(assert v49)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v4a() a1)
+(declare-fun v4b() a0)
+(declare-fun v4c() a1)
+(declare-fun v4d() Int)
+(assert (not (f4 v4a v4b v4c v4d)))
+(assert (= c1$2 v4a))
+(assert (= (c0$4 0) v4b))
+(assert (= c1$2 v4c))
+(assert (= 9 v4d))
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v4e() Bool)
+(declare-fun v4f() a0)
+(declare-fun v50() Bool)
+(declare-fun v51() a1)
+(declare-fun v52() a2)
+(declare-fun v53() a0)
+(declare-fun v54() Int)
+(declare-fun v55() Bool)
+(assert (= (c0$3 c1$4 0 "" 9) (f5 v4e v4f v50 v51 v52 v53 v54 v55)))
+(assert v4e)
+(assert (= (c0$4 0) v4f))
+(assert v50)
+(assert (= c1$2 v51))
+(assert (= (c2$1 ";," c0$0 c1$4) v52))
+(assert (= (c0$4 0) v53))
+(assert (= 9 v54))
+(assert v55)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v56() String)
+(declare-fun v57() Int)
+(declare-fun v58() a1)
+(declare-fun v59() a0)
+(declare-fun v5a() Bool)
+(declare-fun v5b() Int)
+(declare-fun v5c() Int)
+(declare-fun v5d() String)
+(declare-fun v5e() a0)
+(declare-fun v5f() a0)
+(assert true)
+(assert (= "\xc4\xbf)9N\xc2]" v56))
+(assert (= 9 v57))
+(assert (= c1$2 v58))
+(assert (= (c0$4 0) v59))
+(assert v5a)
+(assert (= 9 v5b))
+(assert (= 9 v5c))
+(assert (= "\xc4\xbf)9N\xc2]" v5d))
+(assert (= (c0$4 0) v5e))
+(assert (= (c0$4 0) v5f))
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v60() Bool)
+(declare-fun v61() Bool)
+(declare-fun v62() Int)
+(declare-fun v63() a2)
+(declare-fun v64() Int)
+(declare-fun v65() Int)
+(declare-fun v66() String)
+(declare-fun v67() String)
+(assert true)
+(assert v60)
+(assert v61)
+(assert (= 9 v62))
+(assert (= (c2$1 ";," c0$0 c1$4) v63))
+(assert (= 9 v64))
+(assert (= 9 v65))
+(assert (= "\xc4\xbf)9N\xc2]" v66))
+(assert (= "\xc4\xbf)9N\xc2]" v67))
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v68() a2)
+(declare-fun v69() a1)
+(declare-fun v6a() a0)
+(declare-fun v6b() a2)
+(declare-fun v6c() String)
+(declare-fun v6d() Bool)
+(declare-fun v6e() Int)
+(assert true)
+(assert (= (c2$1 ";," c0$0 c1$4) v68))
+(assert (= c1$2 v69))
+(assert (= (c0$4 0) v6a))
+(assert (= (c2$1 ";," c0$0 c1$4) v6b))
+(assert (= "\xc4\xbf)9N\xc2]" v6c))
+(assert v6d)
+(assert (= 9 v6e))
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v6f() String)
+(declare-fun v70() a1)
+(declare-fun v71() a1)
+(assert true)
+(assert (= "\xc4\xbf)9N\xc2]" v6f))
+(assert (= c1$2 v70))
+(assert (= c1$2 v71))
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun v72() a2)
+(declare-fun v73() Bool)
+(assert (= (c2$1 ";," c0$0 c1$4) (fa v72 v73)))
+(assert (= (c2$1 ";," c0$0 c1$4) v72))
+(assert v73)
+(check-sat)
+(pop 1)
+(exit)

diff --git a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2
index c96ca1bea7af14919730ce8bb75eaae70bf3e388..bf23a9275e859da9e05e5c01aae5793ce455eb3b 100644 (file)
--- a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2
+++ b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -i --strings-exp --no-check-models
+; COMMAND-LINE: -i --strings-exp -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun str7 () String)

diff --git a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2 b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2
index a97863d7db180010f4dbb5c88c1872607cb40f19..c5188e27dd4243c3e70132faef18dd92d88bbf2d 100644 (file)
--- a/test/regress/regress1/strings/strings-leq-trans-unsat.smt2
+++ b/test/regress/regress1/strings/strings-leq-trans-unsat.smt2
@@ -1,5 +1,7 @@
-; COMMAND-LINE: --strings-exp --no-check-unsat-cores
+; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; timeout with unsat cores
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-fun x () String)

diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2
index e7b7547c47411e28196c8163e886c0a2b09e8780..6d028271de40ff8600e79a0b890699643fa2ef26 100644 (file)
--- a/test/regress/regress1/sygus/issue3648.smt2
+++ b/test/regress/regress1/sygus/issue3648.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference
 (set-logic ALL)
 (declare-fun a () Real)
 (assert (> a 0.000001))

diff --git a/test/regress/regress2/bug765.smt2 b/test/regress/regress2/bug765.smt2
index b0d85363d6e7f29b5972c5968ec2a2cae123763a..db87efaa12d87a5253e15fc0a50e79ccbcb9224c 100644 (file)
--- a/test/regress/regress2/bug765.smt2
+++ b/test/regress/regress2/bug765.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --incremental --fmf-fun-rlv -q
 (set-logic ALL)
 
 (declare-datatypes ((Color 0)) (

diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2
index 2d7349c8fed020f4958f47488d53ea2c41b4642f..160074fdef989fc34ec90d078464c5736c7161bc 100644 (file)
--- a/test/regress/regress2/bv_to_int_bitwise.smt2
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -1,11 +1,11 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bv-to-int-use-pow2 --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=5 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bv-to-int-use-pow2 --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=5
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
+; COMMAND-LINE: --solve-bv-as-int=bv
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))

diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
index 2ecd0fe6cd80df6822263182dcd5151228eaa227..5f471e4a9f2f0f3d7f943a8bce38237a220adac5 100644 (file)
--- a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -1,6 +1,7 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
-;COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
-;EXPECT: unsat
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
+; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 (set-logic QF_UFBV)
 (declare-fun z$n0s32 () (_ BitVec 32))
 (declare-fun dataOut () (_ BitVec 32))

diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index c1213809163e2fee54256259942732f7a89c6a75..1b31572772a5288dbb81a857c2eff4ec303de1b5 100644 (file)
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,8 +1,8 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
+; COMMAND-LINE: --solve-bv-as-int=bv
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))

diff --git a/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
index d454ad630c49e4802e6adb62a2346dc86796b9c5..59fa6479f1cb0b89a44a8ed10dd9931bb656e0a1 100644 (file)
--- a/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
+++ b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: (error "Error in option parsing: --solve-bv-as-int=bitwise does not support quantifiers")
 ; EXIT: 1
 (set-logic BV)

diff --git a/test/regress/regress2/fp/issue7056.smt2 b/test/regress/regress2/fp/issue7056.smt2
index 4defecd66f16229ae91d397756b214cf26c241d8..e419a5a6f086c16f00bc37abbdb52d87bbbb7106 100644 (file)
--- a/test/regress/regress2/fp/issue7056.smt2
+++ b/test/regress/regress2/fp/issue7056.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; DISABLE-TESTER: proof
+; DISABLE-TESTER: unsat-core
+; timeout with unsat cores
 (set-logic ALL)
 (set-info :smt-lib-version 2.6)
 (define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))

diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2
index 02f7754cf33c552e5495444a64f0076a66d8fc94..e57acec062e417d8196e71b104d1dd21f83a310a 100644 (file)
--- a/test/regress/regress2/issue3687-check-models.smt2
+++ b/test/regress/regress2/issue3687-check-models.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --check-models
 ; EXPECT: sat
 (set-logic QF_ABV)
 (declare-fun c () (_ BitVec 32))

diff --git a/test/regress/regress2/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2
index dc61155e8c30fe3ea21f33fc67dc509bd167f269..0f67a5a5db18735893d7f44b0866f8c39da1dc49 100644 (file)
--- a/test/regress/regress2/nl/ufnia-factor-open-proof.smt2
+++ b/test/regress/regress2/nl/ufnia-factor-open-proof.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-unsat-cores
 (set-logic QF_UFNIA)
 (set-info :status unsat)
 (declare-fun p2 (Int) Int)

diff --git a/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 b/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
index cdaefbfb93143f2e383ab5d69443aa83ce993a35..eb6e8249891f8ae8fae3f191830ede77290b614e 100644 (file)
--- a/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
+++ b/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --check-unsat-cores --incremental
+; COMMAND-LINE: --incremental
 ; EXPECT: unsat
 ; EXPECT: sat
 ; EXPECT: unsat

diff --git a/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2 b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
index 7f2e3084f9f6ed5f73a5e42a150a753f1ff2313c..20b597da7a9fad7e643d9f17c8d6d5620d6d84e4 100644 (file)
--- a/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
+++ b/test/regress/regress2/quantifiers/exp-trivially-dd3.smt2
@@ -1,6 +1,7 @@
-; COMMAND-LINE: --ee-mode=distributed --no-check-unsat-cores
-; COMMAND-LINE: --ee-mode=central --no-check-unsat-cores
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((dA 0)) (((A))))

diff --git a/test/regress/regress2/strings/issue3203.smt2 b/test/regress/regress2/strings/issue3203.smt2
index f0bc8d031f0a6062e1fc504f2de4b170234f05b5..25785f100ad2f7800ae0056fd3316b43878da41e 100644 (file)
--- a/test/regress/regress2/strings/issue3203.smt2
+++ b/test/regress/regress2/strings/issue3203.smt2
@@ -1,5 +1,5 @@
 ; Temporarily disable checking of unsat cores (see issue #3606)
-; COMMAND-LINE: --no-check-unsat-cores
+; DISABLE-TESTER: unsat-core
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status unsat)

diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
index 8ae10a04f95f48d42af9b5ca41aca0600b0cb2b4..e833fcf8163c15bc9e59164a3ee506049424d3c3 100644 (file)
--- a/test/regress/regress3/bv_to_int_and_or.smt2
+++ b/test/regress/regress3/bv_to_int_and_or.smt2
@@ -1,7 +1,8 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1   --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2   --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=2   --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=2
+; DISABLE-TESTER: proof
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 4))

diff --git a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
index 7fbe5361482e14b74b722f000be4cc12c1e1e3ed..6ba56beb8790d59d17a7f02f69950008368ac766 100644 (file)
--- a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE:  --solve-bv-as-int=sum  --no-check-models
-; COMMAND-LINE:  --solve-bv-as-int=sum  --bv-to-int-use-pow2 --no-check-models
+; COMMAND-LINE:  --solve-bv-as-int=sum 
+; COMMAND-LINE:  --solve-bv-as-int=sum  --bv-to-int-use-pow2
 ; EXPECT: sat
 (set-logic BV)
 (declare-fun s () (_ BitVec 3))

diff --git a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
index b37dc371d5f5dd1f54793780344728cc3e41b450..6f7178a12ab6eed92e683d7df74f31f5194ea2c1 100644 (file)
--- a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE:  --solve-bv-as-int=bv  --no-check-models
-; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all  --no-check-models
+; COMMAND-LINE:  --solve-bv-as-int=bv 
+; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all 
 ;EXPECT: sat
 (set-logic BV)
 (assert (exists ((c__detect__main__1__i_36_C (_ BitVec 32))) (bvslt ((_ sign_extend 32) c__detect__main__1__i_36_C) (_ bv0 64))))

diff --git a/test/regress/regress3/bv_to_int_quant2.smt2 b/test/regress/regress3/bv_to_int_quant2.smt2
index c2bf6d9d05deb58b97bf8ba1669427d4d5acbb63..fe9b69105849fb575724635f9a5fd2fea6118ddc 100644 (file)
--- a/test/regress/regress3/bv_to_int_quant2.smt2
+++ b/test/regress/regress3/bv_to_int_quant2.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=sum --no-check-models
-; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=bv --no-check-models
-; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=iand --no-check-models
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=sum
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=bv
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=iand
 ; EXPECT: sat
 (set-logic BV)
 (declare-fun s () (_ BitVec 4))

diff --git a/test/regress/regress3/issue4476-ext-rew.smt2 b/test/regress/regress3/issue4476-ext-rew.smt2
index 8f1d8285d9947eb6a300e85498dd4cc3af0d67b6..4668e577b173ca54b1dddf06e57a2f60a821cab8 100644 (file)
--- a/test/regress/regress3/issue4476-ext-rew.smt2
+++ b/test/regress/regress3/issue4476-ext-rew.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inst --no-check-models
+; COMMAND-LINE: --sygus-inst
 ; EXPECT: sat
 (set-logic NRA)
 (set-info :status sat)

diff --git a/test/regress/regress3/issue4714.smt2 b/test/regress/regress3/issue4714.smt2
index ac89140443bea6ff4c640ea8f88e3da495782318..b06fd302dc8db589cb4f26bb7f9b635c51b4a8b5 100644 (file)
--- a/test/regress/regress3/issue4714.smt2
+++ b/test/regress/regress3/issue4714.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --check-models
 ; EXPECT: sat 
 (set-logic UFNIRA)
 (declare-fun c (Int) Int)