diff options
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 new file mode 100644 index 000000000..9bc47f925 --- /dev/null +++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 @@ -0,0 +1,11 @@ +; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (choice ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/' +; COMMAND-LINE: --produce-models --model-witness-choice --no-check-models +; EXPECT: sat +; EXPECT: SUCCESS +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun x () Real) +(assert (= (* x x) 2)) +(check-sat) +(get-value (x)) + |