diff options
Diffstat (limited to 'test')
4 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress1/bug516.smt2 b/test/regress/regress1/bug516.smt2 index a01eb97e9..43d18575e 100644 --- a/test/regress/regress1/bug516.smt2 +++ b/test/regress/regress1/bug516.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound-int +; COMMAND-LINE: --finite-model-find --fmf-bound-int -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/model-blocker-values.smt2 b/test/regress/regress1/model-blocker-values.smt2 index 65db79ca4..1c9e80642 100644 --- a/test/regress/regress1/model-blocker-values.smt2 +++ b/test/regress/regress1/model-blocker-values.smt2 @@ -1,7 +1,8 @@ ; COMMAND-LINE: --incremental --produce-models --block-models=values ; EXPECT: sat ; EXPECT: sat -; EXPECT: sat +; if we only block models restricted to (a,b), then there are only 2 models +; EXPECT: unsat (set-logic QF_UFLIA) (declare-fun a () Int) (declare-fun b () Int) diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 index fdbac9996..585ea0602 100644 --- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 +++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv +; COMMAND-LINE: --cegqi-bv -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2 index 28e999604..e1a923f98 100644 --- a/test/regress/regress1/quantifiers/issue3664.smt2 +++ b/test/regress/regress1/quantifiers/issue3664.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun-rlv --sygus-inference +; COMMAND-LINE: --fmf-fun-rlv --sygus-inference --no-check-models ; EXPECT: sat (set-logic QF_NRA) (declare-fun a () Real) |