7 files changed, 114 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 20272de2b..35d604768 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -3,6 +3,12 @@
 
 set(regress_0_tests
   regress0/arith/ackermann.real.smt2
+  regress0/arith/arith-eq.smt2
+  regress0/arith/arith-mixed.smt2
+  regress0/arith/arith-tighten-1.smt2
+  regress0/arith/arith-strict.smt2
+  regress0/arith/arith-mixed-types-tighten.smt2
+  regress0/arith/arith-mixed-types-no-tighten.smt2
   regress0/arith/arith.01.cvc
   regress0/arith/arith.02.cvc
   regress0/arith/arith.03.cvc
diff --git a/test/regress/regress0/arith/arith-eq.smt2 b/test/regress/regress0/arith/arith-eq.smt2
new file mode 100644
index 000000000..661c3f242
--- /dev/null
+++ b/test/regress/regress0/arith/arith-eq.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+(assert (= z 0))
+(assert (= (* 3 x) y))
+(assert (= (+ 1 (* 5 x)) y))
+(assert (= (+ 7 (* 4 x)) y))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
new file mode 100644
index 000000000..a06621224
--- /dev/null
+++ b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun x () Real)
+(declare-fun n () Int)
+
+; Even though `n` is an integer, this would be UNSAT for real `n`, so the integrality can be ignored.
+(assert
+    (and
+        (>= (+ x n) 1)
+        (<= n 0)
+        (<= x 0)
+    )
+)
+
+(check-sat)
+
diff --git a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
new file mode 100644
index 000000000..2f737d5c5
--- /dev/null
+++ b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
@@ -0,0 +1,32 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun x_44 () Real)
+(declare-fun x_45 () Real)
+
+; This test is a subset of one of the `../lemmas` tests. I think `../lemmas/sc_init_frame_gap.induction.smtv1.smt2`.
+(declare-fun termITE_30 () Int)
+(declare-fun termITE_3 () Real)
+(declare-fun termITE_4 () Real)
+(declare-fun termITE_8 () Real)
+(declare-fun termITE_9 () Real)
+(declare-fun termITE_31 () Int)
+
+(assert
+    (let ((_let_0 (* (- 1.0) termITE_3)))
+        (and
+            (>= (+ termITE_8 (* (- 1.0) termITE_9)) 0.0)
+            ; This literal can be tightened to `termITE_31 <= 1`.
+            (not (>= termITE_31 2))
+            (>= (+ (* (- 1.0) x_44) (/ termITE_31 1)) 0.0)
+            (>= (+ x_44 (* (- 1.0) termITE_4)) 0.0)
+            (not (>= (+ _let_0 (* (/ 1 2) termITE_8)) 0.0))
+            (>= (+ (* (- 1.0) x_45) termITE_9) 0.0)
+            (>= (+ x_45 (/ (* (- 1) termITE_30) 1)) 0.0)
+            (>= termITE_30 2)
+            (>= (+ _let_0 termITE_4) 0.0)))
+)
+
+(check-sat)
+
diff --git a/test/regress/regress0/arith/arith-mixed.smt2 b/test/regress/regress0/arith/arith-mixed.smt2
new file mode 100644
index 000000000..5869a51bd
--- /dev/null
+++ b/test/regress/regress0/arith/arith-mixed.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+; Both strict and non-strict inequalities.
+(assert (< y 0))
+(assert (>= y x))
+(assert (>= y (- x)))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-strict.smt2 b/test/regress/regress0/arith/arith-strict.smt2
new file mode 100644
index 000000000..969cfd0bb
--- /dev/null
+++ b/test/regress/regress0/arith/arith-strict.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+(assert (< y 0))
+(assert (> y x))
+(assert (> y (- x)))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/arith-tighten-1.smt2 b/test/regress/regress0/arith/arith-tighten-1.smt2
new file mode 100644
index 000000000..237d5b144
--- /dev/null
+++ b/test/regress/regress0/arith/arith-tighten-1.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun n () Int)
+
+; tests tightenings of the form [Int] >= r   to [Int] >= ceiling(r)
+; where r is a real.
+(assert
+    (and
+        (>= n 1.5)
+        (<= n 1.9)
+    )
+)
+
+(check-sat)
+