More check models (#6439)

diff --git a/test/regress/regress0/arith/ackermann.real.smt2 b/test/regress/regress0/arith/ackermann.real.smt2
index 00dd79ebefc8196f08eea83771d6d910187b5fb4..e0f3b85f949e9a92304efcb1cec1a4fca06a652d 100644 (file)
--- a/test/regress/regress0/arith/ackermann.real.smt2
+++ b/test/regress/regress0/arith/ackermann.real.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --ackermann  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFNRA)
 

diff --git a/test/regress/regress0/arith/integers/ackermann1.smt2 b/test/regress/regress0/arith/integers/ackermann1.smt2
index b04210f3638c318a658381ece176ccd853f943fd..677ba24ff8c401212a837bf7178910eb3ba1df4b 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann1.smt2
+++ b/test/regress/regress0/arith/integers/ackermann1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --ackermann  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFLIA)
 

diff --git a/test/regress/regress0/arith/integers/ackermann2.smt2 b/test/regress/regress0/arith/integers/ackermann2.smt2
index f20fd99bfca4f99621ec3450106baf6081b12fb4..3013071f9aefcfd3d6cdab4e8f9cc6af3f39f989 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann2.smt2
+++ b/test/regress/regress0/arith/integers/ackermann2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --ackermann  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFLIA)
 

diff --git a/test/regress/regress0/arith/integers/ackermann3.smt2 b/test/regress/regress0/arith/integers/ackermann3.smt2
index 4b4137cb9f93685c2f2b9df1de60824638503b58..cf35267689793d3f210d4ee3276d97d3a1410618 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann3.smt2
+++ b/test/regress/regress0/arith/integers/ackermann3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --ackermann  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFLIA)
 

diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2
index bf55b41c23b4c1176eef52479a4c6f61161670f7..14af6b6ad77e50a2d14ba23d04fcaabc74cadf12 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann4.smt2
+++ b/test/regress/regress0/arith/integers/ackermann4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_ALIA)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2
index 8d6f124cd0a1695d2c180de6c808bd080868713b..d5099a6d92ed544f12a885bd9b82626504761767 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann5.smt2
+++ b/test/regress/regress0/arith/integers/ackermann5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models
+; COMMAND-LINE: --ackermann
 ; EXPECT: sat
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2
index 96bf547033ba44ddd2b3fd78b1dc375d03b422fb..cae429f938801e3ccf7c352d7257f59bf0cfc112 100644 (file)
--- a/test/regress/regress0/arith/integers/ackermann6.smt2
+++ b/test/regress/regress0/arith/integers/ackermann6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index 9bba5f141601b7a63aae9d8aaf636d43a5e7721a..5eea40acb02eb8b5fc6339417f5601b105d90369 100644 (file)
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager  --no-check-unsat-cores
 ; REQUIRES: cryptominisat
 ; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat

diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2
index 9b44b8d634794f4d12be2c6287f9dd237b5a7236..8eb5ca70ac012f170ee9fef242104087177263ae 100644 (file)
--- a/test/regress/regress0/bv/ackermann3.smt2
+++ b/test/regress/regress0/bv/ackermann3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_ABV)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/regress0/bv/ackermann5.smt2 b/test/regress/regress0/bv/ackermann5.smt2
index 240691cd38431d29fe878286f757c3ac8a0174fb..44d0f4dab8a5189582234e13dc99f62b1bed1cac 100644 (file)
--- a/test/regress/regress0/bv/ackermann5.smt2
+++ b/test/regress/regress0/bv/ackermann5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 

diff --git a/test/regress/regress0/bv/ackermann6.smt2 b/test/regress/regress0/bv/ackermann6.smt2
index 20e0c638c1b2b13869f84f9493895db6ac16a48a..8be60bf806731155b367e6e42977d1b8a2fb0671 100644 (file)
--- a/test/regress/regress0/bv/ackermann6.smt2
+++ b/test/regress/regress0/bv/ackermann6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 

diff --git a/test/regress/regress0/bv/ackermann7.smt2 b/test/regress/regress0/bv/ackermann7.smt2
index 3b901d5527d66b70285e721db433a58310e62973..2d43bc6068dd700707326ed40ea6e96bb2c80bbf 100644 (file)
--- a/test/regress/regress0/bv/ackermann7.smt2
+++ b/test/regress/regress0/bv/ackermann7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 

diff --git a/test/regress/regress0/bv/ackermann8.smt2 b/test/regress/regress0/bv/ackermann8.smt2
index 91c13b056a78374f46f68f4a19e888025c39d112..5ca49011f9eac69d9db61851345637eece9a0807 100644 (file)
--- a/test/regress/regress0/bv/ackermann8.smt2
+++ b/test/regress/regress0/bv/ackermann8.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 

diff --git a/test/regress/regress0/bv/bv-abstr-bug.smt2 b/test/regress/regress0/bv/bv-abstr-bug.smt2
index 745996cb75e6ff6bc658b431eff0bb1c1ae5a150..cc38075a9bddfc91d9142e5497f056669e90cce9 100644 (file)
--- a/test/regress/regress0/bv/bv-abstr-bug.smt2
+++ b/test/regress/regress0/bv/bv-abstr-bug.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-abstraction --bitblast=eager --no-check-models
+; COMMAND-LINE: --bv-abstraction --bitblast=eager
 ;
 ; BV-abstraction should not be applied
 (set-logic QF_BV)

diff --git a/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
index 1ef63f365068df35c1bff17faacd65d21d08a80c..15f80f209f13cc1b1d75070cf2e78f3abb156161 100644 (file)
--- a/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
+++ b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models 
+; COMMAND-LINE: --solve-int-as-bv=4 
 ; EXPECT: sat
 (set-logic ALL)
 (declare-sort S 0)

diff --git a/test/regress/regress0/fmf/fd-false.smt2 b/test/regress/regress0/fmf/fd-false.smt2
index 4e1ff64b53838807e8a0fef7c7230d8727966c04..0d8737a90b30447a7b32918b8ceb21481327817a 100644 (file)
--- a/test/regress/regress0/fmf/fd-false.smt2
+++ b/test/regress/regress0/fmf/fd-false.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (define-fun-rec f ((x Int)) Bool false)

diff --git a/test/regress/regress0/issue4010-sort-inf-var.smt2 b/test/regress/regress0/issue4010-sort-inf-var.smt2
index 5b953e204efdc4693470fb19781890c6e62c8a91..d261b38193443475ce69cd2027d8a8f00429caed 100644 (file)
--- a/test/regress/regress0/issue4010-sort-inf-var.smt2
+++ b/test/regress/regress0/issue4010-sort-inf-var.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sort-inference --no-check-models
+; COMMAND-LINE: --sort-inference
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress0/issue4469-unc-no-reuse-var.smt2 b/test/regress/regress0/issue4469-unc-no-reuse-var.smt2
index 3bc79578f334f80a067acb70b1bfb63a0e991176..dacf43b91e250c884946df63462f96150a568625 100644 (file)
--- a/test/regress/regress0/issue4469-unc-no-reuse-var.smt2
+++ b/test/regress/regress0/issue4469-unc-no-reuse-var.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 ; EXPECT: sat
 (set-logic QF_AUFBVLIA)
 (declare-fun a () Int)

diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2
index 52bb2596394f4ec3d37efb41d25154a5067a530e..99f975e412dfdfc9a4c9db120969e6916507f7de 100644 (file)
--- a/test/regress/regress0/nl/issue3003.smt2
+++ b/test/regress/regress0/nl/issue3003.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/nl/issue3407.smt2 b/test/regress/regress0/nl/issue3407.smt2
index e4be74c8a22c6d2413656ed48853178e6e8c3809..6f12f3528d4d447e1d0b34941454cc5716cf272c 100644 (file)
--- a/test/regress/regress0/nl/issue3407.smt2
+++ b/test/regress/regress0/nl/issue3407.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic NRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/quantifiers/delta-simp.smt2 b/test/regress/regress0/quantifiers/delta-simp.smt2
index e5883134f74514ab286e9328832728741dd2afda..bc08b905384e9f4981733bec19443ced4809bae3 100644 (file)
--- a/test/regress/regress0/quantifiers/delta-simp.smt2
+++ b/test/regress/regress0/quantifiers/delta-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic LRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
index fd7b3f574dc9219f61d3492b5ce41a862f28b092..82a81f4bce8fbb9eda4e26ed222f80a9d1e1189d 100644 (file)
--- a/test/regress/regress0/quantifiers/mix-complete-strat.smt2
+++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi --finite-model-find --no-check-models
+; COMMAND-LINE: --cegqi --finite-model-find
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)

diff --git a/test/regress/regress0/quantifiers/mix-simp.smt2 b/test/regress/regress0/quantifiers/mix-simp.smt2
index b7142c6e9c20635c01dd1302cbd763d7fcfd4bab..feda1174038e2cf65270358d3705d0ff8507dbf9 100644 (file)
--- a/test/regress/regress0/quantifiers/mix-simp.smt2
+++ b/test/regress/regress0/quantifiers/mix-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic LIRA)
 (set-info :status sat)

diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
index efac3468c3872e7aff5b0034e478ca5c0ff018f1..67fb5bf24b47ca21589e79eb646410ee3edc9524 100644 (file)
--- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi --no-check-models
+; COMMAND-LINE: --cegqi
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)

diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2
index fd951c7abaed107bbdbc7ce4adc12668344ad524..93fed02b8ce85251289a79e42be8363651bb5a35 100644 (file)
--- a/test/regress/regress0/unconstrained/arith.smt2
+++ b/test/regress/regress0/unconstrained/arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2
index bf9f34298bd47c986f5e63d34e695e68a6632410..d664647a5f2b0b337d01eb7582c6a1fbcef60b83 100644 (file)
--- a/test/regress/regress0/unconstrained/arith2.smt2
+++ b/test/regress/regress0/unconstrained/arith2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2
index edf0d4cdf37463e6e7f72a086776851c36db2395..f75ab9b0ca9c8a8c3160d627dfa55be1dd51fd39 100644 (file)
--- a/test/regress/regress0/unconstrained/arith3.smt2
+++ b/test/regress/regress0/unconstrained/arith3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2
index f68ebf88a3b0261ba46c8b78658031f54c073cb3..5bb5f1eeee593f0da0983dcfff220078b119eec0 100644 (file)
--- a/test/regress/regress0/unconstrained/arith4.smt2
+++ b/test/regress/regress0/unconstrained/arith4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFNIRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2
index cc19b5389774416032797d1c1d818d3fb5808002..f821004057f217c0ae2649d5ef20afb8bcb088a6 100644 (file)
--- a/test/regress/regress0/unconstrained/arith5.smt2
+++ b/test/regress/regress0/unconstrained/arith5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2
index 24e57b0f71c93482f0a250df2810e9519537ccb4..0e4ab2e0f8daefed699101c3a6951d80d9e6504f 100644 (file)
--- a/test/regress/regress0/unconstrained/arith6.smt2
+++ b/test/regress/regress0/unconstrained/arith6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2
index 5fe0618035d09691b6bdf65728a94ed7e440cd7f..4ed0aa17fa8bb3f9859fe0202b9cc77d46672300 100644 (file)
--- a/test/regress/regress0/unconstrained/arith7.smt2
+++ b/test/regress/regress0/unconstrained/arith7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2
index 5c8ff51472f3be0a9f5cdd4167074f243234bd09..9b8a57e2d76243a52bb72b098b46e39e33f71b36 100644 (file)
--- a/test/regress/regress0/unconstrained/array1.smt2
+++ b/test/regress/regress0/unconstrained/array1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBV)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2
index 9964aa728c76126dbc09df5bd057589d84bcf7aa..4e8921eadd2f120245a86fb8d567ebee60281602 100644 (file)
--- a/test/regress/regress0/unconstrained/bvbool.smt2
+++ b/test/regress/regress0/unconstrained/bvbool.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2
index 788a0578b2ec70fbb7b310abd04a5ecd763beac6..7ebc28d7f3445e364e65ef67d12eaf6c73c5ae6f 100644 (file)
--- a/test/regress/regress0/unconstrained/bvbool2.smt2
+++ b/test/regress/regress0/unconstrained/bvbool2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2
index 524fdd107ec70d60523e508cce2eebf6c38c2012..9931e99f79b3fe713241b5d09d1ac7c9ff3eeeaf 100644 (file)
--- a/test/regress/regress0/unconstrained/bvbool3.smt2
+++ b/test/regress/regress0/unconstrained/bvbool3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2
index 5a6c314bd5d30e50e0fa478a0e62665e1fb6f181..438944900817e5111f2aaa5f92eb1fbbc3e7e845 100644 (file)
--- a/test/regress/regress0/unconstrained/bvcmp.smt2
+++ b/test/regress/regress0/unconstrained/bvcmp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2
index c93189837573b217be1a8bb10a1e03e38467aad2..98b33b727b8caf1879f71b57886335f346349f5a 100644 (file)
--- a/test/regress/regress0/unconstrained/bvconcat.smt2
+++ b/test/regress/regress0/unconstrained/bvconcat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2
index 9e9ac87d30c577f684250948a23563b9f3b70ffe..869b6644bf965b69d673240068d0bc15f577a49f 100644 (file)
--- a/test/regress/regress0/unconstrained/bvconcat2.smt2
+++ b/test/regress/regress0/unconstrained/bvconcat2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2
index 2c2b4d5f805d1aab6fd3f3b0f20363390fffd01a..d65e912c06e3e560491a5fa2ddf89af87b5ab15c 100644 (file)
--- a/test/regress/regress0/unconstrained/bvdiv.smt2
+++ b/test/regress/regress0/unconstrained/bvdiv.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2
index dd4de72514568e1d437bf7b6d54ebe377b5a0daa..057a61fae2d1b6323c11914a3eb6b59376c91e5c 100644 (file)
--- a/test/regress/regress0/unconstrained/bvext.smt2
+++ b/test/regress/regress0/unconstrained/bvext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2
index f89dd6b6b47b5a61614567370288937369141214..1c6f9254b61c22bd87e735dc38e5b9a324ca1127 100644 (file)
--- a/test/regress/regress0/unconstrained/bvite.smt2
+++ b/test/regress/regress0/unconstrained/bvite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2
index c26304073846c9aa67703efbd57a3febaeaf05fd..06b6770a0373b2b3bf34d7c23bb79d8d82ff7b8a 100644 (file)
--- a/test/regress/regress0/unconstrained/bvmul.smt2
+++ b/test/regress/regress0/unconstrained/bvmul.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2
index fd8cc1e3db608808033294c236b0f48a015c63f7..62fc5f123f1fe6acb6b70cec0280b6e0bce5f5e9 100644 (file)
--- a/test/regress/regress0/unconstrained/bvmul2.smt2
+++ b/test/regress/regress0/unconstrained/bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2
index e3894408202cbad54e4006f724745d37ca43a588..23d66ea6c546ccbc1271370666369e2b48046695 100644 (file)
--- a/test/regress/regress0/unconstrained/bvmul3.smt2
+++ b/test/regress/regress0/unconstrained/bvmul3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2
index cdeb77a3baf7fba4e0539c2ab7a885b2b1adae2a..48a9fa151e4f2a65a419fac00aa9138cfb4321cb 100644 (file)
--- a/test/regress/regress0/unconstrained/bvnot.smt2
+++ b/test/regress/regress0/unconstrained/bvnot.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2
index 594ed0c4d64301662bf92befc3e23436ad5a7b59..e566045a7d4687d42979370cb78ef2211004104c 100644 (file)
--- a/test/regress/regress0/unconstrained/bvsle.smt2
+++ b/test/regress/regress0/unconstrained/bvsle.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2
index fe4c4d4b4bd790a644f8107df4590e95dece264b..707ab4893f8c624b28f62fc83b3b856c10f95aeb 100644 (file)
--- a/test/regress/regress0/unconstrained/bvsle2.smt2
+++ b/test/regress/regress0/unconstrained/bvsle2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2
index 5d8359e3120066ceeee106a229b613817a73db9b..0194ee3f79551b2b8f1889382bfb92dccdb2e301 100644 (file)
--- a/test/regress/regress0/unconstrained/bvsle3.smt2
+++ b/test/regress/regress0/unconstrained/bvsle3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2
index 0c60acfcbcafd812d4aa0714499b13efff92661c..b390c67c4e4e5e9ea47aaa19fc01bd22f0bd730d 100644 (file)
--- a/test/regress/regress0/unconstrained/bvsle4.smt2
+++ b/test/regress/regress0/unconstrained/bvsle4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2
index e8027465f91ed50a70b9a455cca135336bd852d5..c292cc1a3737f9daed29a524625d261d37e12081 100644 (file)
--- a/test/regress/regress0/unconstrained/bvsle5.smt2
+++ b/test/regress/regress0/unconstrained/bvsle5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2
index 191038a4cfffabb45102a93217af8a6f122be642..0c474bd65868b9d06172ae2d542f8694d3aac3b7 100644 (file)
--- a/test/regress/regress0/unconstrained/bvslt.smt2
+++ b/test/regress/regress0/unconstrained/bvslt.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2
index a22e51cc66225c89932c82182711323580924e0f..29882d9f8f830308457c59c9a61b066623f60322 100644 (file)
--- a/test/regress/regress0/unconstrained/bvslt2.smt2
+++ b/test/regress/regress0/unconstrained/bvslt2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2
index e702379ac2f73c168078228a67d207ed36b3ba1d..ad8cd5216ea0c888d20780af9356728a899e3542 100644 (file)
--- a/test/regress/regress0/unconstrained/bvslt3.smt2
+++ b/test/regress/regress0/unconstrained/bvslt3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2
index bdda57a8d98239cea6b1c2e7acd4c244c963eb2b..86e1f57390a80c13c43c48c79361d3fd4c7e4da0 100644 (file)
--- a/test/regress/regress0/unconstrained/bvslt4.smt2
+++ b/test/regress/regress0/unconstrained/bvslt4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2
index 2dbe3645cc804658dfb03fee1e5137fad2af5141..25d7b4a1ea213d890b523c2468cc2efe27b784a0 100644 (file)
--- a/test/regress/regress0/unconstrained/bvslt5.smt2
+++ b/test/regress/regress0/unconstrained/bvslt5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2
index 58e8f2796dc88d0ad9b6a41258cda5e86f7949bf..b6bc67d7fc831b37fa466ba6fb017ec8e2a737f3 100644 (file)
--- a/test/regress/regress0/unconstrained/bvule.smt2
+++ b/test/regress/regress0/unconstrained/bvule.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2
index f3dd4860e9f84b8850ae204adc3546c691a135d7..cb22b89f32f736192d7578f0aa24e63476cd65bb 100644 (file)
--- a/test/regress/regress0/unconstrained/bvule2.smt2
+++ b/test/regress/regress0/unconstrained/bvule2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2
index e16baff0280c585fdd4e31a12bdb6a665423fddd..dfd5a45c3012aec52b97cf65a2e0a479f0486690 100644 (file)
--- a/test/regress/regress0/unconstrained/bvule3.smt2
+++ b/test/regress/regress0/unconstrained/bvule3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2
index 564db97486eb16c4ab24b91c5803e0ed324069db..2f37edbc236f6525602a14a0e67f4dfe7178aedf 100644 (file)
--- a/test/regress/regress0/unconstrained/bvule4.smt2
+++ b/test/regress/regress0/unconstrained/bvule4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2
index 70ac8910fadd19fc2d8865fad444a43ab70808ea..4a7ba96553b7608e6f2bee3e2222ba88dd435e4b 100644 (file)
--- a/test/regress/regress0/unconstrained/bvule5.smt2
+++ b/test/regress/regress0/unconstrained/bvule5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2
index 44bdefd625e87951e34b5804e9184d6297561878..50fb93cc907f2decc0459a1930e935f544fa42ec 100644 (file)
--- a/test/regress/regress0/unconstrained/bvult.smt2
+++ b/test/regress/regress0/unconstrained/bvult.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2
index f8eee92f61bbf8e8b37ef3c4c3871cf73e1ccf92..84769899ffc71460c7155b608982220510880ac7 100644 (file)
--- a/test/regress/regress0/unconstrained/bvult2.smt2
+++ b/test/regress/regress0/unconstrained/bvult2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2
index 43f79a5691725c61f4ab21b619c5e95696ae232b..40666a5df7a6bc2bf7f39063404abbf274069dad 100644 (file)
--- a/test/regress/regress0/unconstrained/bvult3.smt2
+++ b/test/regress/regress0/unconstrained/bvult3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2
index fe716b13930a4d6f2abc77053901ad861f6e4dd4..d59d8601d4f6e9fe2e7c5808505e08df9624402d 100644 (file)
--- a/test/regress/regress0/unconstrained/bvult4.smt2
+++ b/test/regress/regress0/unconstrained/bvult4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2
index 151db6f02976d328d1784c82b432984891151b7e..9823aaf679f9a70d3077ac061c1037dda137fc3e 100644 (file)
--- a/test/regress/regress0/unconstrained/bvult5.smt2
+++ b/test/regress/regress0/unconstrained/bvult5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2
index e84876133cfbdc10bd25adfe98a2d2f1df138854..f332630a28ae7be2963859c3be8a7721eaa00286 100644 (file)
--- a/test/regress/regress0/unconstrained/geq.smt2
+++ b/test/regress/regress0/unconstrained/geq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2
index 2c118cd9c12687cd317fd62673b1ad807c0ca8fd..a73994cc9fa5bf08a2e561b02e84f79b13c74b39 100644 (file)
--- a/test/regress/regress0/unconstrained/gt.smt2
+++ b/test/regress/regress0/unconstrained/gt.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/ite.smt2 b/test/regress/regress0/unconstrained/ite.smt2
index 54f092b8c6d3c31402863bdd8e002eef91fb7638..827960f07e906173c5fc8b97eb0192a24abc5b5a 100644 (file)
--- a/test/regress/regress0/unconstrained/ite.smt2
+++ b/test/regress/regress0/unconstrained/ite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBV )
 (set-info :status sat)
 (declare-sort U 0)

diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2
index ed568c5fd95afabdb078799f64abbeb69d571512..9df62394af6e3a043ff28a2add19cfbb614eaeee 100644 (file)
--- a/test/regress/regress0/unconstrained/leq.smt2
+++ b/test/regress/regress0/unconstrained/leq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2
index 06724ad45ab9871940ea73746b293603c9e2d016..95b4ebfaf6ddb7aa0098391a64e77662d8ebaf74 100644 (file)
--- a/test/regress/regress0/unconstrained/lt.smt2
+++ b/test/regress/regress0/unconstrained/lt.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/mult1.smt2 b/test/regress/regress0/unconstrained/mult1.smt2
index 4a29d9a92436001666acffc75cef6e96ab183c60..50d097946f55df3617246c5260035e3799458d71 100644 (file)
--- a/test/regress/regress0/unconstrained/mult1.smt2
+++ b/test/regress/regress0/unconstrained/mult1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_LIA)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2
index f85054926b3cfb3039c565e3a98dee3026cc6414..3631295453e4f107a97f2725782a7df06864242c 100644 (file)
--- a/test/regress/regress0/unconstrained/uf1.smt2
+++ b/test/regress/regress0/unconstrained/uf1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2
index cb0b39040e0c5ef93e0295f40f21abe416b60418..0d16b58cc0ecbf0d3a4a399f9d1db21d029923a8 100644 (file)
--- a/test/regress/regress0/unconstrained/xor.smt2
+++ b/test/regress/regress0/unconstrained/xor.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --unconstrained-simp --no-check-models
+; COMMAND-LINE: --unconstrained-simp
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/regress1/bug519.smt2 b/test/regress/regress1/bug519.smt2
index 2d7d3a9c5405a9d4dd8001c9bda7e71ec7272476..6f413ad8bd7f06a13f0f650dd4edd851dc74ab19 100644 (file)
--- a/test/regress/regress1/bug519.smt2
+++ b/test/regress/regress1/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi -mi --no-check-models
+; COMMAND-LINE: --cegqi -mi
 ; EXPECT: sat
 ; EXPECT: unsat
 

diff --git a/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
index f7c13722b5bf318c4dbda9b47a3a0fc11213a993..9bb1fcb552a7bf13171e50f449b357b14be0eaef 100644 (file)
--- a/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
+++ b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --fmf-fun-rlv
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)

diff --git a/test/regress/regress1/fmf/ALG008-1.smt2 b/test/regress/regress1/fmf/ALG008-1.smt2
index 5bf36a715602d80f50a2489d0426279fdc787962..8c8cdf92ae8368d139925011e32f2cb0db6b0ab2 100644 (file)
--- a/test/regress/regress1/fmf/ALG008-1.smt2
+++ b/test/regress/regress1/fmf/ALG008-1.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --finite-model-find
-; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
+; COMMAND-LINE: --finite-model-find --sort-inference
 ; EXPECT: sat
 ;%--------------------------------------------------------------------------
 ;% File     : ALG008-1 : TPTP v5.4.0. Released v2.2.0.

diff --git a/test/regress/regress1/fmf/issue4068-si-qf.smt2 b/test/regress/regress1/fmf/issue4068-si-qf.smt2
index de6da315f4fd42875aacbf412214eb5385291853..efe25da5b25fc902e45f898faf3341280320a6b9 100644 (file)
--- a/test/regress/regress1/fmf/issue4068-si-qf.smt2
+++ b/test/regress/regress1/fmf/issue4068-si-qf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --sort-inference --no-check-models
+; COMMAND-LINE: --fmf-fun --sort-inference
 ; EXPECT: sat
 (set-logic QF_UFNIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/nlp042+1.smt2 b/test/regress/regress1/fmf/nlp042+1.smt2
index 6159f0b4106f4c87c9f3fde7bd384a6afd10126a..352ee9f482bc0f2da6c51544eb19b786a1953587 100644 (file)
--- a/test/regress/regress1/fmf/nlp042+1.smt2
+++ b/test/regress/regress1/fmf/nlp042+1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --no-check-models
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-logic UF)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/pow2-bool.smt2 b/test/regress/regress1/fmf/pow2-bool.smt2
index 4943c646cfd148c4538f5b7433df77e5535ca1bd..93814578dae54415ab0a06f6dd0f35f2a1bb0eae 100644 (file)
--- a/test/regress/regress1/fmf/pow2-bool.smt2
+++ b/test/regress/regress1/fmf/pow2-bool.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun -q
 ; EXPECT: sat
 (set-logic ALL)
 

diff --git a/test/regress/regress1/fmf/sort-inf-int-real.smt2 b/test/regress/regress1/fmf/sort-inf-int-real.smt2
index 9944ee55c0bbd29be2d15a83def0453389a3470f..0d0a9eccc2330712271ca5b7afbb36cc75442e5d 100644 (file)
--- a/test/regress/regress1/fmf/sort-inf-int-real.smt2
+++ b/test/regress/regress1/fmf/sort-inf-int-real.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
+; COMMAND-LINE: --finite-model-find --sort-inference
 ; EXPECT: sat
 (set-logic UFLIRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/sort-inf-int.smt2 b/test/regress/regress1/fmf/sort-inf-int.smt2
index e4a8978d4a4cfb5dbcefce1d9e0af9229ef82522..ba859aba95fce27d57583d09dd55801bc64f4ddf 100644 (file)
--- a/test/regress/regress1/fmf/sort-inf-int.smt2
+++ b/test/regress/regress1/fmf/sort-inf-int.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --sort-inference --no-check-models
+; COMMAND-LINE: --finite-model-find --sort-inference
 ; EXPECT: sat
 (set-logic UFLIRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
index 9dd95aeae3894a86205f937976840595d37b9757..61f0f207be0f0093903d89bbd7602fd9696d80ac 100644 (file)
--- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
+++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --uf-ho --finite-model-find --no-check-models
+; COMMAND-LINE: --uf-ho --finite-model-find -q
 ; EXPECT: sat
 
 (set-logic ALL)
@@ -32,4 +32,4 @@
 
 
 
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2
index 96f52fd397094162c343a0d87ffd6477c4e417fc..d3066c2824c289c8590f2f3f863e96e264968f92 100644 (file)
--- a/test/regress/regress1/ho/issue4092-sinf.smt2
+++ b/test/regress/regress1/ho/issue4092-sinf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --uf-ho --sort-inference --no-check-models
+; COMMAND-LINE: --uf-ho --sort-inference
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :sort-inference true)

diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2
index e87845fabeb74c200580260c99ac1ec12b5d02e2..60a754aadc8add9abd30fe65aaec2e9d3a80290b 100644 (file)
--- a/test/regress/regress1/ho/issue4134-sinf.smt2
+++ b/test/regress/regress1/ho/issue4134-sinf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --uf-ho --sort-inference --no-check-models
+; COMMAND-LINE: --uf-ho --sort-inference
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :uf-ho true)

diff --git a/test/regress/regress1/nl/factor_agg_s.smt2 b/test/regress/regress1/nl/factor_agg_s.smt2
index 4497f4c298147cbe7a96ff45b54e85b35a9df725..1f6f6ea4ecee40497e46ff5baab9988cc39e5967 100644 (file)
--- a/test/regress/regress1/nl/factor_agg_s.smt2
+++ b/test/regress/regress1/nl/factor_agg_s.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --decision=justification --no-check-models
+; COMMAND-LINE: --decision=justification
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress1/nl/iand-native-1.smt2
index 051264cfc27ac0578686d44da1a1284cc0a3e5f3..0835b70662b63a84d8c03e1e3a7adbaf186983de 100644 (file)
--- a/test/regress/regress1/nl/iand-native-1.smt2
+++ b/test/regress/regress1/nl/iand-native-1.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --iand-mode=value --no-check-models
-; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find --no-check-models
+; COMMAND-LINE: --iand-mode=value
+; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find
 ; COMMAND-LINE: --iand-mode=bitwise
 ; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=1
 ; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=2

diff --git a/test/regress/regress1/nl/iand-native-granularities.smt2 b/test/regress/regress1/nl/iand-native-granularities.smt2
index 92cdfb1abb443eb3a847fc721cae47d3baeb194f..e895663f8217c5c3d97b4277bd48217abbff104e 100644 (file)
--- a/test/regress/regress1/nl/iand-native-granularities.smt2
+++ b/test/regress/regress1/nl/iand-native-granularities.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --iand-mode=value --no-check-models
-; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find --no-check-models
+; COMMAND-LINE: --iand-mode=value
+; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find
 ; COMMAND-LINE: --iand-mode=bitwise
 ; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=1
 ; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=3

diff --git a/test/regress/regress1/nl/issue3307.smt2 b/test/regress/regress1/nl/issue3307.smt2
index 803bfeb3a8fbaf9ea14036da161a44240a6dc87f..c4301a3eacd1fc5cb9e2b053a06520aac0e8ddfc 100644 (file)
--- a/test/regress/regress1/nl/issue3307.smt2
+++ b/test/regress/regress1/nl/issue3307.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic NRA)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/RND-small.smt2 b/test/regress/regress1/quantifiers/RND-small.smt2
index cf5c3bc7ed45a8e79b6c8258b72d4c3d061c0fbc..22dc1d209d4b084b87ad196c3e1395b8e9b6b9e9 100644 (file)
--- a/test/regress/regress1/quantifiers/RND-small.smt2
+++ b/test/regress/regress1/quantifiers/RND-small.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic LRA)
 (declare-fun y1 () Real)

diff --git a/test/regress/regress1/quantifiers/issue3316.smt2 b/test/regress/regress1/quantifiers/issue3316.smt2
index 0e69410f7f6626ea8529789b1e296a15919b185f..2fc38f4b47d59229000c792c5aa963bd3b060661 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3316.smt2
+++ b/test/regress/regress1/quantifiers/issue3316.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --fmf-fun-rlv
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)

diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
index 2024153ad885383493099cf20ace5766e1e239ce..7f0ab060f854569b8ba2988b091e9cd1bd3c7d28 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3537.smt2
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-check-models --finite-model-find
+; COMMAND-LINE: --strings-exp --finite-model-find
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((UNIT 0)) (((Unit))

diff --git a/test/regress/regress1/quantifiers/issue3765-quant-dd.smt2 b/test/regress/regress1/quantifiers/issue3765-quant-dd.smt2
index 624e5ddfa872487c719e17faba94b6b92f47d9de..d4013bc40f738e88136a02706f68752e6c653c70 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3765-quant-dd.smt2
+++ b/test/regress/regress1/quantifiers/issue3765-quant-dd.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --no-check-models
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 
 (set-logic ALL)

diff --git a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
index eaf4a3427815327be05ef2daa9c5cf020143dca0..1b4bd0d7f370c6fe310b4e8f1ee0e73c03e73cc0 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
+++ b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models --sygus-inst
+; COMMAND-LINE: --arith-rewrite-equalities --global-negate --sygus-inst
 ; EXPECT: sat
 (set-logic NIA)
 (set-option :arith-rewrite-equalities true)

diff --git a/test/regress/regress1/quantifiers/psyco-196.smt2 b/test/regress/regress1/quantifiers/psyco-196.smt2
index fef1a24c63c6bbb03b5a9102882b8a71d602a1a0..f2c9317178c7cc97f874fb7d5db14a48a1a4657e 100644 (file)
--- a/test/regress/regress1/quantifiers/psyco-196.smt2
+++ b/test/regress/regress1/quantifiers/psyco-196.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic LIA)
 (set-info :status sat)

diff --git a/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 b/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
index 05bcb762fe2b91f7dc128f1c4b465631a0e218c6..9a19cb7851d6db66382c4664897fed3bd454ce6f 100644 (file)
--- a/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
+++ b/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --no-check-models
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)

diff --git a/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 b/test/regress/regress1/quantifiers/sygus-infer-nested.smt2
index a1e449fa3925f7956c106db6f1813305334f2fff..7d14ee0944cc18e28eda74828948ba16bec0bfa3 100644 (file)
--- a/test/regress/regress1/quantifiers/sygus-infer-nested.smt2
+++ b/test/regress/regress1/quantifiers/sygus-infer-nested.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference -q
 (set-logic LIA)
 (set-info :status sat)
 (assert (forall ((x Int) (y Int)) (or (<= x (+ y 1)) (exists ((z Int)) (and (> z y) (< z x))))))

diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2
index fac9d6b9d08828609257133d9bc59f1179756327..ce16e6f14ee5e03cd570185d8a9c6bb1c4312f4b 100644 (file)
--- a/test/regress/regress1/sep/finite-witness-sat.smt2
+++ b/test/regress/regress1/sep/finite-witness-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models
+; COMMAND-LINE: --finite-model-find --quant-epr
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (declare-sort Loc 0)

diff --git a/test/regress/regress1/sep/sep-fmf-priority.smt2 b/test/regress/regress1/sep/sep-fmf-priority.smt2
index 8aed931190d295a78006e52be9c1bbf215c69284..d916a50e529876b4e21f4f82bbc95e97a4358fc8 100644 (file)
--- a/test/regress/regress1/sep/sep-fmf-priority.smt2
+++ b/test/regress/regress1/sep/sep-fmf-priority.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models
+; COMMAND-LINE: --finite-model-find --quant-epr
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 

diff --git a/test/regress/regress1/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2
index 60ab5d038c7f5d797f1c5be7cc00570c7baae172..ff725f048bf3a8762facaf44c2061ee33d49bab4 100644 (file)
--- a/test/regress/regress1/sep/split-find-unsat.smt2
+++ b/test/regress/regress1/sep/split-find-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: unsat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)

diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2
index da1d8bd51414cf0db5f0663a9bf2424af94cd75e..dabdc18e4cff5b0a47aa308abd106fa0c374dd0d 100644 (file)
--- a/test/regress/regress1/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress1/sep/wand-simp-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE:
 ; EXPECT: unsat
 (set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)

diff --git a/test/regress/regress1/sets/choose.cvc b/test/regress/regress1/sets/choose.cvc
index 2112e702b331662c502b375c0d561e6bd873dcb6..a8c5b249576122ae3f0d50c7f3b4dc27cc3bb85c 100644 (file)
--- a/test/regress/regress1/sets/choose.cvc
+++ b/test/regress/regress1/sets/choose.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --no-check-models
+% COMMAND-LINE:
 % EXPECT: sat
 
 A : SET OF INT;

diff --git a/test/regress/regress1/sqrt2-sort-inf-unk.smt2 b/test/regress/regress1/sqrt2-sort-inf-unk.smt2
index d9489eee7d3db5ea1fc6722bf5692b1bae9d998e..00f49dde00839deb7b4bb3c188f96dc43c81dc47 100644 (file)
--- a/test/regress/regress1/sqrt2-sort-inf-unk.smt2
+++ b/test/regress/regress1/sqrt2-sort-inf-unk.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sort-inference --no-check-models
+; COMMAND-LINE: --sort-inference
 ; EXPECT: sat
 (set-logic QF_NRA)
 (declare-fun x () Real)

diff --git a/test/regress/regress1/sygus/issue3498.smt2 b/test/regress/regress1/sygus/issue3498.smt2
index 9fa8fdc1e3f1ebf08f9225fcd2a57a486c90fa4d..b04407c93a91ee65a393b6747024e51188ab62de 100644 (file)
--- a/test/regress/regress1/sygus/issue3498.smt2
+++ b/test/regress/regress1/sygus/issue3498.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference
 (set-logic ALL)
 (declare-fun x () Real)
 (assert (= x 1))

diff --git a/test/regress/regress1/sygus/issue3514.smt2 b/test/regress/regress1/sygus/issue3514.smt2
index c643e7d5ade9a5ddd537abd325cc0a9a9192eddb..c5e39d93ad983b79180583790b351e8667aa954c 100644 (file)
--- a/test/regress/regress1/sygus/issue3514.smt2
+++ b/test/regress/regress1/sygus/issue3514.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference -q
 (set-logic ALL)
 (assert
  (forall ((a Real))

diff --git a/test/regress/regress1/sygus/issue3644.smt2 b/test/regress/regress1/sygus/issue3644.smt2
index 60c6ea4eea7434fd2a72b9064c58debddde0f0c8..234bf406782c339651524127697c884b38bec8fd 100644 (file)
--- a/test/regress/regress1/sygus/issue3644.smt2
+++ b/test/regress/regress1/sygus/issue3644.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference -q
 (set-logic LIA)
 (assert (forall ((a Int)) (=> (> a 0) (exists ((b Int)) (> a (* b 2))))))
 (check-sat)

diff --git a/test/regress/regress2/quantifiers/gn-wrong-091018.smt2 b/test/regress/regress2/quantifiers/gn-wrong-091018.smt2
index 733180faa6f8ffff613f36ad0902ad68424b4416..5ca44f16d39d4b3b56e2d788e2770eec7cac1fdb 100644 (file)
--- a/test/regress/regress2/quantifiers/gn-wrong-091018.smt2
+++ b/test/regress/regress2/quantifiers/gn-wrong-091018.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --global-negate --no-check-models
+; COMMAND-LINE: --global-negate
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic BV)

diff --git a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
index 72743693a39c61f1b3460f37b48fce0ce8f08fb5..b076b730d39cefb10854bd8c6d956ef72f545b41 100644 (file)
--- a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
+++ b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-all --no-check-models
+; COMMAND-LINE: --cegqi-all
 ; EXPECT: sat
 ;AJR:BROKEN
 (set-logic UFBV)