diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 10:52:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-14 10:52:01 -0500 |
| commit | ad8729d3a0060ed635b8a82e9ed323966cc2f49d (patch) | |
| tree | 78c5ea5b46bf22498801328f706b9f94a572c1e2 /test/regress/regress0/dump-unsat-core-full.smt2 | |
| parent | 3b36892dec58f945b7e724395c53a288f9d2d0ef (diff) | |
Fix dump-unsat-cores-full (#4303)
This adds a fix to ensure dump-unsat-cores-full works by modifying the public options function. This options currently does not work since dumpUnsatCores is only set internally now. This fix is only required until options are refactored so that SmtEngine owns the authoritative copy of options.
Diffstat (limited to 'test/regress/regress0/dump-unsat-core-full.smt2')
| -rw-r--r-- | test/regress/regress0/dump-unsat-core-full.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/dump-unsat-core-full.smt2 b/test/regress/regress0/dump-unsat-core-full.smt2 new file mode 100644 index 000000000..3c68501f9 --- /dev/null +++ b/test/regress/regress0/dump-unsat-core-full.smt2 @@ -0,0 +1,12 @@ +; REQUIRES: proof +; COMMAND-LINE: --dump-unsat-cores-full +; EXPECT: unsat +; EXPECT: ( +; EXPECT: (and (= x y) (< x y)) +; EXPECT: ) +(set-logic QF_LIA) +(set-info :status unsat) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (and (= x y) (< x y))) +(check-sat) |