diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-07 11:26:31 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-07 18:26:31 +0000 |
| commit | e5e727c868e169028bb24ca4547ba7078d366161 (patch) | |
| tree | 81316c41bac8cdd0539b53c4ba85ca25d62b85d1 /examples | |
| parent | cb20e47bc69a6bdf00ab255ed23b3cfd9c26c10b (diff) | |
Add a binary / SMT-LIB quickstart (#7315)
This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/api/smtlib/quickstart.smt2 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/examples/api/smtlib/quickstart.smt2 b/examples/api/smtlib/quickstart.smt2 index c1597aa5c..b5dc87d2b 100644 --- a/examples/api/smtlib/quickstart.smt2 +++ b/examples/api/smtlib/quickstart.smt2 @@ -1,11 +1,11 @@ (set-logic ALL) (set-option :produce-models true) -(set-option :produce-unsat-cores true) (set-option :incremental true) -; necessary to print in the unsat core assertions that do not have names +; print unsat cores, include assertions in the unsat core that have not been named +(set-option :produce-unsat-cores true) (set-option :dump-unsat-cores-full true) -; Declare real constanst x,y +; Declare real constants x,y (declare-const x Real) (declare-const y Real) @@ -27,7 +27,7 @@ (echo "We will reset the solver with the (reset-assertions) command and check satisfiability of the same assertions but with the integers constants rather than with the real ones.") (reset-assertions) -; Declare integer constanst a,b +; Declare integer constants a,b (declare-const a Int) (declare-const b Int) (assert (< 0 a)) |