From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 18:59:56 +0000 (-0600)
Subject: Clean usage of options in regressions (#8190)
X-Git-Tag: cvc5-1.0.0~343
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4ca634218d48a79983ee789fb132d3ffa5ea872f;p=cvc5.git

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 5a410ba2d..22718ae04 100644
--- 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 8854db877..555b35a36 100644
--- 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 153d5bc37..06467a24a 100644
--- 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 a4921e5c9..cc52cc126 100644
--- 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 c9a84d1ec..99bedad3a 100644
--- 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 14af6b6ad..50ff90e22 100644
--- 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 3f23e0367..11734fbc6 100644
--- 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 abe5b09fd..52e15a366 100644
--- 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 7de7aebc8..2e71b26d5 100644
--- 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 d84041fc9..757c14b91 100644
--- 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 ad967b48f..5532d39d2 100644
--- 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 8d0f81f80..5fc4d828b 100644
--- 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 88cbd8a0b..fefb3c059 100644
--- 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
index 72942a24e..000000000
--- 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 97b891415..7f2d0dece 100644
--- 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 f70dc4a3d..545f558f2 100644
--- 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 8eb5ca70a..3893c2e7b 100644
--- 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 ad65d8ca4..3e4898d45 100644
--- 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 dc2cb7f35..03ff10903 100644
--- 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 eced6e0e9..614e2bb16 100644
--- 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 ebe8ab10c..c139c7858 100644
--- 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 d4ad9695f..b3f4c6e80 100644
--- 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 6d2971ad8..307cd1a49 100644
--- 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 65471a6b9..1900ddcb1 100644
--- 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 16fdc2b77..254b8c3b3 100644
--- 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 011b7432e..fcbd5dbde 100644
--- 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 ac9de97d2..35d6e5d30 100644
--- 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 ebbe07519..36495b5ed 100644
--- 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 faf72f0e1..765bcdc2c 100644
--- 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 06c1415c2..42c2513f1 100644
--- 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 603c783d3..81531b293 100644
--- 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 20170ea1b..da53e24da 100644
--- 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 4b120fc9d..3f637cd34 100644
--- 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 9ee1fa5eb..58b007053 100644
--- 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 05ca33aac..8f9dbd29e 100644
--- 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 1e30a7ee8..bf6cc1cb7 100644
--- 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 46c08dad5..0acf5af2e 100644
--- 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 dd4d4f951..e0244b419 100644
--- 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 b53f0fbef..644723916 100644
--- 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 4fbcfb00b..a5c736323 100644
--- 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 0fbf4edeb..96f44f9dc 100644
--- 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 5724d7fa7..5ef198120 100644
--- 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 cef646f16..0aed32ddd 100644
--- 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 4b3bdd067..ede4fc368 100644
--- 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 75d4b6e3a..69bb74e84 100644
--- 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 c006b2885..c9337beb5 100644
--- 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 01930da6d..f5a462d9a 100644
--- 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 69c36179a..8fd7ec018 100644
--- 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 e7446a8c0..cf4ec5cfb 100644
--- 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 96a1d86ba..ab10a29a5 100644
--- 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 217d12cd3..5fac95767 100644
--- 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 a3f64d2b1..c1ca4f015 100644
--- 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 372e8f1f3..14d3605d7 100644
--- 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 f16c6fb90..6d0adceda 100644
--- 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 15ee0e7cf..cc89b7829 100644
--- 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 488c558b0..1dac5a805 100644
--- 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 2d35a43d8..7f811f796 100644
--- 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 953c5252d..0b47edc63 100644
--- 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 a8039ce5b..49390f937 100644
--- 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 1c690cc75..698fedc76 100644
--- 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 d84d900f3..eae46e0e5 100644
--- 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 8f6a16b45..7d3a7a2d9 100644
--- 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 9ee7e8fa0..5c194ffad 100644
--- 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 071122e4f..3297fa830 100644
--- 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 ff22a3288..af637e2bc 100644
--- 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 238fec914..0422e099c 100644
--- 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 e8d1efe51..3a88e75a3 100644
--- 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 9bb1fcb55..31e4ca4d8 100644
--- 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 1bf48a1b2..2ae2bccf9 100644
--- 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 b35c98aa9..ab0490b9b 100644
--- 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 956a55cd3..b9734b1e5 100644
--- 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 8a853c4b6..f5970a741 100644
--- 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 cb55d8504..5187f4a25 100644
--- 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 dba8a05ae..395c68382 100644
--- 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 efcae64bc..0ec2b5c28 100644
--- 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 32e9d4178..35a247689 100644
--- 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 479769188..33c932915 100644
--- 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 6a8feba5c..e7fe960ea 100644
--- 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 3f02e56fd..e77caa315 100644
--- 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 5d036a84f..8cdbddc8a 100644
--- 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 b5ab4609b..25cb0810c 100644
--- 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 86e3a6d6f..be2482eb1 100644
--- 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 221a5613d..7a969a3b4 100644
--- 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 f3faceda5..96cf7dc91 100644
--- 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 8074fb2f2..106b75f3c 100644
--- 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 3a4a23dbb..fa9616847 100644
--- 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 f863842de..8af32cde1 100644
--- 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 d29a16313..30a6554c1 100644
--- 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 4fb0732a3..267a012cf 100644
--- 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 9c1d9cef6..cf8dd7f91 100644
--- 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 fde3b9a81..e08d1607a 100644
--- 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 7cacfca98..20dcc2931 100644
--- 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 2b5c6cab9..472168f00 100644
--- 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 2fc38f4b4..e4bdcda04 100644
--- 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 758878af2..0df91e9d2 100644
--- 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 9843b92ff..f4831fd6f 100644
--- 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 e1a923f98..ebb89a4c9 100644
--- 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 4947586f2..dedb43a48 100644
--- 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
-; 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)
+; 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 f3a3c99b7..46bd7a178 100644
--- 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 fa9691578..3fe54e2c6 100644
--- 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 d66afb91a..3549a770f 100644
--- 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 0cd319ffb..e60500833 100644
--- 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 9ccde98cd..64e0c0529 100644
--- 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 b428cc52a..30cb757c2 100644
--- 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 b7cc50885..6ef920613 100644
--- 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 39b92a6ad..13c675609 100644
--- 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 55338bf6c..9b2d1161e 100644
--- 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 fc22a8af8..e7be953ce 100644
--- 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 39790c38d..10aefca49 100644
--- 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 465408cc5..fee303330 100644
--- 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 241f69b77..c83952562 100644
--- 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 e9915bf4b..f50f9301f 100644
--- 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 c40106c48..f1e81d38e 100644
--- 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 c6d239ec0..d12e9d638 100644
--- 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 867d4ccb8..6e281fb66 100644
--- 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 e66a39f23..7f11186fe 100644
--- 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 dc114b0dd..ca718df1b 100644
--- 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 b34e6031f..8a47fc7f7 100644
--- 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 0b38bd189..b3fbf7e10 100644
--- 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 eee6fa211..e6aefc698 100644
--- 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 612776cfa..6b8c771ac 100644
--- 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 334908e64..999a08060 100644
--- 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 3d496782c..69bd9fcf5 100644
--- 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 4239a415e..ecd842766 100644
--- 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 15362f227..8db329e92 100644
--- 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 79c12c028..91782600e 100644
--- 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 76aed570f..cdb69d95b 100644
--- 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 0fc0e8b53..ec948d55a 100644
--- 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
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-; EXPECT: sat
-
-; 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)
+; 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 c96ca1bea..bf23a9275 100644
--- 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 a97863d7d..c5188e27d 100644
--- 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 e7b7547c4..6d028271d 100644
--- 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 b0d85363d..db87efaa1 100644
--- 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 2d7349c8f..160074fde 100644
--- 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 2ecd0fe6c..5f471e4a9 100644
--- 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 c12138091..1b3157277 100644
--- 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 d454ad630..59fa6479f 100644
--- 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 4defecd66..e419a5a6f 100644
--- 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 02f7754cf..e57acec06 100644
--- 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 dc61155e8..0f67a5a5d 100644
--- 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 cdaefbfb9..eb6e82498 100644
--- 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 7f2e3084f..20b597da7 100644
--- 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 f0bc8d031..25785f100 100644
--- 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 8ae10a04f..e833fcf81 100644
--- 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 7fbe53614..6ba56beb8 100644
--- 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 b37dc371d..6f7178a12 100644
--- 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 c2bf6d9d0..fe9b69105 100644
--- 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 8f1d8285d..4668e577b 100644
--- 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 ac8914044..b06fd302d 100644
--- 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)