From 73289d1ded3b68e5ea8175f6b089ca7f0314dd35 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 8 Feb 2022 13:45:26 -0500
Subject: [PATCH] test: regressions test for LRA

---
 tests/unsat/reg_lra_3.smt2 |  9 +++++++++
 tests/unsat/reg_lra_4.smt2 | 12 ++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 tests/unsat/reg_lra_3.smt2
 create mode 100644 tests/unsat/reg_lra_4.smt2

diff --git a/tests/unsat/reg_lra_3.smt2 b/tests/unsat/reg_lra_3.smt2
new file mode 100644
index 00000000..d8be54cd
--- /dev/null
+++ b/tests/unsat/reg_lra_3.smt2
@@ -0,0 +1,9 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLRA)
+(set-info :source |modified from smtlib.626179.smt2|)
+(set-info :status unsat)
+(declare-fun f3 () Real)
+(declare-fun f4 () Real)
+(assert (not (=> (< f3 f4) (=> (< f4 (* 2.0 f3)) (< 0.0 (- f4 f3))))))
+(check-sat)
+(exit)
diff --git a/tests/unsat/reg_lra_4.smt2 b/tests/unsat/reg_lra_4.smt2
new file mode 100644
index 00000000..be98bfce
--- /dev/null
+++ b/tests/unsat/reg_lra_4.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_LRA)
+(set-info :status unsat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+
+(assert (<= a b))
+(assert (= p1 (>= a 1)))
+(assert (= p2 (<= b (/ 1 2))))
+(check-sat-assuming (p1 p2))
+(exit)