diff options
Diffstat (limited to 'examples/api/smtlib/linear_arith.smt2')
-rw-r--r-- | examples/api/smtlib/linear_arith.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/examples/api/smtlib/linear_arith.smt2 b/examples/api/smtlib/linear_arith.smt2 new file mode 100644 index 000000000..ede655b0e --- /dev/null +++ b/examples/api/smtlib/linear_arith.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_LIRA) +(declare-const x Int) +(declare-const y Real) +(assert + (and + (>= x (* 3 y)) + (<= x y) + (< (- 2) x) + ) +) +(push 1) +(echo "Checking entailement by asserting the negation") +(echo "Unsat == ENTAILED") +(assert (not (<= (- y x) (/ 2 3)))) +(check-sat) +(pop 1) +(push 1) +(echo "Checking that the assertions are consistent") +(assert (= (- y x) (/ 2 3))) +(check-sat) +(pop 1) |