add some incremental in-tree regressions

1 files changed, 18 insertions, 0 deletions

diff --git a/test/regress/regress0/uflia/check04.smt2 b/test/regress/regress0/uflia/check04.smt2
new file mode 100644
index 000000000..61bc8a5d6
--- /dev/null
+++ b/test/regress/regress0/uflia/check04.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_LIA)
+(declare-fun _b () Int)
+(declare-fun _n () Int)
+(declare-fun _x () Bool)
+
+(assert (<= 2 _n))
+(assert  (not (= _b 0)))
+
+(push 1)
+(assert (or (= _n 1) (or _x (= _b 0))))
+(check-sat)
+(pop 1)
+
+(assert (or (= _n 1) (or _x (= _b 0))))
+
+(assert (or (not _x) (= _n 1)))
+
+(check-sat)