diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/quantifiers/cegqi-nl-simp.cvc | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3647.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/sin1-deq-sat.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/sin1-sat.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3648.smt2 | 2 |
5 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc index d01d7b7d2..eaefbe651 100644 --- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc +++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc @@ -1,2 +1,3 @@ +% COMMAND-LINE: --nl-rlv=none % EXPECT: entailed QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ; diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2 index 0fc0f55f9..6c66d2e4c 100644 --- a/test/regress/regress1/nl/issue3647.smt2 +++ b/test/regress/regress1/nl/issue3647.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-models --produce-models --decision=internal +; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2 index d9e12c7b4..4fb0732a3 100644 --- a/test/regress/regress1/nl/sin1-deq-sat.smt2 +++ b/test/regress/regress1/nl/sin1-deq-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2 index d2a21fa60..9c1d9cef6 100644 --- a/test/regress/regress1/nl/sin1-sat.smt2 +++ b/test/regress/regress1/nl/sin1-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2 index e7b7547c4..2fc1a6115 100644 --- a/test/regress/regress1/sygus/issue3648.smt2 +++ b/test/regress/regress1/sygus/issue3648.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference --no-check-models +; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always (set-logic ALL) (declare-fun a () Real) (assert (> a 0.000001)) |