From dce2fd01164df92e66e94c5aee4f95491d3ab5d9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 25 Apr 2021 14:56:01 -0500 Subject: [PATCH] More check models (#6439) --- test/regress/regress0/arith/ackermann.real.smt2 | 2 +- test/regress/regress0/arith/integers/ackermann1.smt2 | 2 +- test/regress/regress0/arith/integers/ackermann2.smt2 | 2 +- test/regress/regress0/arith/integers/ackermann3.smt2 | 2 +- test/regress/regress0/arith/integers/ackermann4.smt2 | 2 +- test/regress/regress0/arith/integers/ackermann5.smt2 | 2 +- test/regress/regress0/arith/integers/ackermann6.smt2 | 2 +- test/regress/regress0/bv/ackermann2.smt2 | 2 +- test/regress/regress0/bv/ackermann3.smt2 | 2 +- test/regress/regress0/bv/ackermann5.smt2 | 2 +- test/regress/regress0/bv/ackermann6.smt2 | 2 +- test/regress/regress0/bv/ackermann7.smt2 | 2 +- test/regress/regress0/bv/ackermann8.smt2 | 2 +- test/regress/regress0/bv/bv-abstr-bug.smt2 | 2 +- test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 | 2 +- test/regress/regress0/fmf/fd-false.smt2 | 2 +- test/regress/regress0/issue4010-sort-inf-var.smt2 | 2 +- test/regress/regress0/issue4469-unc-no-reuse-var.smt2 | 2 +- test/regress/regress0/nl/issue3003.smt2 | 2 +- test/regress/regress0/nl/issue3407.smt2 | 2 +- test/regress/regress0/quantifiers/delta-simp.smt2 | 2 +- test/regress/regress0/quantifiers/mix-complete-strat.smt2 | 2 +- test/regress/regress0/quantifiers/mix-simp.smt2 | 2 +- test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 | 2 +- test/regress/regress0/unconstrained/arith.smt2 | 2 +- test/regress/regress0/unconstrained/arith2.smt2 | 2 +- test/regress/regress0/unconstrained/arith3.smt2 | 2 +- test/regress/regress0/unconstrained/arith4.smt2 | 2 +- test/regress/regress0/unconstrained/arith5.smt2 | 2 +- test/regress/regress0/unconstrained/arith6.smt2 | 2 +- test/regress/regress0/unconstrained/arith7.smt2 | 2 +- test/regress/regress0/unconstrained/array1.smt2 | 2 +- test/regress/regress0/unconstrained/bvbool.smt2 | 2 +- test/regress/regress0/unconstrained/bvbool2.smt2 | 2 +- test/regress/regress0/unconstrained/bvbool3.smt2 | 2 +- test/regress/regress0/unconstrained/bvcmp.smt2 | 2 +- test/regress/regress0/unconstrained/bvconcat.smt2 | 2 +- test/regress/regress0/unconstrained/bvconcat2.smt2 | 2 +- test/regress/regress0/unconstrained/bvdiv.smt2 | 2 +- test/regress/regress0/unconstrained/bvext.smt2 | 2 +- test/regress/regress0/unconstrained/bvite.smt2 | 2 +- test/regress/regress0/unconstrained/bvmul.smt2 | 2 +- test/regress/regress0/unconstrained/bvmul2.smt2 | 2 +- test/regress/regress0/unconstrained/bvmul3.smt2 | 2 +- test/regress/regress0/unconstrained/bvnot.smt2 | 2 +- test/regress/regress0/unconstrained/bvsle.smt2 | 2 +- test/regress/regress0/unconstrained/bvsle2.smt2 | 2 +- test/regress/regress0/unconstrained/bvsle3.smt2 | 2 +- test/regress/regress0/unconstrained/bvsle4.smt2 | 2 +- test/regress/regress0/unconstrained/bvsle5.smt2 | 2 +- test/regress/regress0/unconstrained/bvslt.smt2 | 2 +- test/regress/regress0/unconstrained/bvslt2.smt2 | 2 +- test/regress/regress0/unconstrained/bvslt3.smt2 | 2 +- test/regress/regress0/unconstrained/bvslt4.smt2 | 2 +- test/regress/regress0/unconstrained/bvslt5.smt2 | 2 +- test/regress/regress0/unconstrained/bvule.smt2 | 2 +- test/regress/regress0/unconstrained/bvule2.smt2 | 2 +- test/regress/regress0/unconstrained/bvule3.smt2 | 2 +- test/regress/regress0/unconstrained/bvule4.smt2 | 2 +- test/regress/regress0/unconstrained/bvule5.smt2 | 2 +- test/regress/regress0/unconstrained/bvult.smt2 | 2 +- test/regress/regress0/unconstrained/bvult2.smt2 | 2 +- test/regress/regress0/unconstrained/bvult3.smt2 | 2 +- test/regress/regress0/unconstrained/bvult4.smt2 | 2 +- test/regress/regress0/unconstrained/bvult5.smt2 | 2 +- test/regress/regress0/unconstrained/geq.smt2 | 2 +- test/regress/regress0/unconstrained/gt.smt2 | 2 +- test/regress/regress0/unconstrained/ite.smt2 | 2 +- test/regress/regress0/unconstrained/leq.smt2 | 2 +- test/regress/regress0/unconstrained/lt.smt2 | 2 +- test/regress/regress0/unconstrained/mult1.smt2 | 2 +- test/regress/regress0/unconstrained/uf1.smt2 | 2 +- test/regress/regress0/unconstrained/xor.smt2 | 2 +- test/regress/regress1/bug519.smt2 | 2 +- test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 | 2 +- test/regress/regress1/fmf/ALG008-1.smt2 | 2 +- test/regress/regress1/fmf/issue4068-si-qf.smt2 | 2 +- test/regress/regress1/fmf/nlp042+1.smt2 | 2 +- test/regress/regress1/fmf/pow2-bool.smt2 | 2 +- test/regress/regress1/fmf/sort-inf-int-real.smt2 | 2 +- test/regress/regress1/fmf/sort-inf-int.smt2 | 2 +- test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 | 4 ++-- test/regress/regress1/ho/issue4092-sinf.smt2 | 2 +- test/regress/regress1/ho/issue4134-sinf.smt2 | 2 +- test/regress/regress1/nl/factor_agg_s.smt2 | 2 +- test/regress/regress1/nl/iand-native-1.smt2 | 4 ++-- test/regress/regress1/nl/iand-native-granularities.smt2 | 4 ++-- test/regress/regress1/nl/issue3307.smt2 | 2 +- test/regress/regress1/quantifiers/RND-small.smt2 | 2 +- test/regress/regress1/quantifiers/issue3316.smt2 | 2 +- test/regress/regress1/quantifiers/issue3537.smt2 | 2 +- test/regress/regress1/quantifiers/issue3765-quant-dd.smt2 | 2 +- test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 | 2 +- test/regress/regress1/quantifiers/psyco-196.smt2 | 2 +- .../regress1/quantifiers/small-pipeline-fixpoint-3.smt2 | 2 +- test/regress/regress1/quantifiers/sygus-infer-nested.smt2 | 2 +- test/regress/regress1/sep/finite-witness-sat.smt2 | 2 +- test/regress/regress1/sep/sep-fmf-priority.smt2 | 2 +- test/regress/regress1/sep/split-find-unsat.smt2 | 2 +- test/regress/regress1/sep/wand-simp-unsat.smt2 | 2 +- test/regress/regress1/sets/choose.cvc | 2 +- test/regress/regress1/sqrt2-sort-inf-unk.smt2 | 2 +- test/regress/regress1/sygus/issue3498.smt2 | 2 +- test/regress/regress1/sygus/issue3514.smt2 | 2 +- test/regress/regress1/sygus/issue3644.smt2 | 2 +- test/regress/regress2/quantifiers/gn-wrong-091018.smt2 | 2 +- test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 | 2 +- 107 files changed, 110 insertions(+), 110 deletions(-) diff --git a/test/regress/regress0/arith/ackermann.real.smt2 b/test/regress/regress0/arith/ackermann.real.smt2 index 00dd79ebe..e0f3b85f9 100644 --- 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 b04210f36..677ba24ff 100644 --- 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 f20fd99bf..3013071f9 100644 --- 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 4b4137cb9..cf3526768 100644 --- 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 bf55b41c2..14af6b6ad 100644 --- 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 8d6f124cd..d5099a6d9 100644 --- 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 96bf54703..cae429f93 100644 --- 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 9bba5f141..5eea40acb 100644 --- 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 9b44b8d63..8eb5ca70a 100644 --- 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 240691cd3..44d0f4dab 100644 --- 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 20e0c638c..8be60bf80 100644 --- 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 3b901d552..2d43bc606 100644 --- 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 91c13b056..5ca49011f 100644 --- 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 745996cb7..cc38075a9 100644 --- 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 1ef63f365..15f80f209 100644 --- 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 4e1ff64b5..0d8737a90 100644 --- 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 5b953e204..d261b3819 100644 --- 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 3bc79578f..dacf43b91 100644 --- 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 52bb25963..99f975e41 100644 --- 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 e4be74c8a..6f12f3528 100644 --- 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 e5883134f..bc08b9053 100644 --- 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 fd7b3f574..82a81f4bc 100644 --- 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 b7142c6e9..feda11740 100644 --- 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 efac3468c..67fb5bf24 100644 --- 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 fd951c7ab..93fed02b8 100644 --- 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 bf9f34298..d664647a5 100644 --- 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 edf0d4cdf..f75ab9b0c 100644 --- 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 f68ebf88a..5bb5f1eee 100644 --- 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 cc19b5389..f82100405 100644 --- 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 24e57b0f7..0e4ab2e0f 100644 --- 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 5fe061803..4ed0aa17f 100644 --- 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 5c8ff5147..9b8a57e2d 100644 --- 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 9964aa728..4e8921ead 100644 --- 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 788a0578b..7ebc28d7f 100644 --- 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 524fdd107..9931e99f7 100644 --- 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 5a6c314bd..438944900 100644 --- 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 c93189837..98b33b727 100644 --- 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 9e9ac87d3..869b6644b 100644 --- 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 2c2b4d5f8..d65e912c0 100644 --- 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 dd4de7251..057a61fae 100644 --- 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 f89dd6b6b..1c6f9254b 100644 --- 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 c26304073..06b6770a0 100644 --- 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 fd8cc1e3d..62fc5f123 100644 --- 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 e38944082..23d66ea6c 100644 --- 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 cdeb77a3b..48a9fa151 100644 --- 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 594ed0c4d..e566045a7 100644 --- 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 fe4c4d4b4..707ab4893 100644 --- 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 5d8359e31..0194ee3f7 100644 --- 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 0c60acfcb..b390c67c4 100644 --- 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 e8027465f..c292cc1a3 100644 --- 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 191038a4c..0c474bd65 100644 --- 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 a22e51cc6..29882d9f8 100644 --- 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 e702379ac..ad8cd5216 100644 --- 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 bdda57a8d..86e1f5739 100644 --- 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 2dbe3645c..25d7b4a1e 100644 --- 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 58e8f2796..b6bc67d7f 100644 --- 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 f3dd4860e..cb22b89f3 100644 --- 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 e16baff02..dfd5a45c3 100644 --- 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 564db9748..2f37edbc2 100644 --- 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 70ac8910f..4a7ba9655 100644 --- 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 44bdefd62..50fb93cc9 100644 --- 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 f8eee92f6..84769899f 100644 --- 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 43f79a569..40666a5df 100644 --- 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 fe716b139..d59d8601d 100644 --- 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 151db6f02..9823aaf67 100644 --- 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 e84876133..f332630a2 100644 --- 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 2c118cd9c..a73994cc9 100644 --- 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 54f092b8c..827960f07 100644 --- 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 ed568c5fd..9df62394a 100644 --- 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 06724ad45..95b4ebfaf 100644 --- 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 4a29d9a92..50d097946 100644 --- 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 f85054926..363129545 100644 --- 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 cb0b39040..0d16b58cc 100644 --- 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 2d7d3a9c5..6f413ad8b 100644 --- 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 f7c13722b..9bb1fcb55 100644 --- 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 5bf36a715..8c8cdf92a 100644 --- 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 de6da315f..efe25da5b 100644 --- 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 6159f0b41..352ee9f48 100644 --- 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 4943c646c..93814578d 100644 --- 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 9944ee55c..0d0a9eccc 100644 --- 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 e4a8978d4..ba859aba9 100644 --- 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 9dd95aeae..61f0f207b 100644 --- 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 96f52fd39..d3066c282 100644 --- 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 e87845fab..60a754aad 100644 --- 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 4497f4c29..1f6f6ea4e 100644 --- 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 051264cfc..0835b7066 100644 --- 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 92cdfb1ab..e895663f8 100644 --- 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 803bfeb3a..c4301a3ea 100644 --- 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 cf5c3bc7e..22dc1d209 100644 --- 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 0e69410f7..2fc38f4b4 100644 --- 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 2024153ad..7f0ab060f 100644 --- 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 624e5ddfa..d4013bc40 100644 --- 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 eaf4a3427..1b4bd0d7f 100644 --- 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 fef1a24c6..f2c931717 100644 --- 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 05bcb762f..9a19cb785 100644 --- 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 a1e449fa3..7d14ee094 100644 --- 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 fac9d6b9d..ce16e6f14 100644 --- 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 8aed93119..d916a50e5 100644 --- 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 60ab5d038..ff725f048 100644 --- 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 da1d8bd51..dabdc18e4 100644 --- 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 2112e702b..a8c5b2495 100644 --- 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 d9489eee7..00f49dde0 100644 --- 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 9fa8fdc1e..b04407c93 100644 --- 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 c643e7d5a..c5e39d93a 100644 --- 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 60c6ea4ee..234bf4067 100644 --- 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 733180faa..5ca44f16d 100644 --- 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 72743693a..b076b730d 100644 --- 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) -- 2.30.2