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)