diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 09:02:15 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 09:02:15 -0600 |
| commit | abd0048cdb6cf4d2ee0a096c9f7a63a1f7f1d9c8 (patch) | |
| tree | cffa12338950b4d7b5bfc43e78849684b6058e30 /test | |
| parent | 50c31e61ab240ccd551a0aea732f8b9a88d7fb32 (diff) | |
Support for witnessing choice in models (#3781)
Fixes #3300.
This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b909817df..6acc6f7c8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1306,6 +1306,7 @@ set(regress_1_tests regress1/nl/exp1-lb.smt2 regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 + regress1/nl/issue3300-approx-sqrt-witness.smt2 regress1/nl/issue3441.smt2 regress1/nl/issue3617.smt2 regress1/nl/issue3656.smt2 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)) + |