Tests: Add test for incremental solving with theory combination

usi-verification-and-security · May 7, 2024 · 9168c12 · 9168c12
1 parent 7f764cd
commit 9168c12
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git a/regression/QF_UFLRA/incremental.smt2 b/regression/QF_UFLRA/incremental.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_UFLRA)
+(declare-fun f (Real) Real)
+(declare-fun y () Real)
+(declare-fun x () Real)
+(assert (not (= (f x) (f y))))
+(push 1)
+(assert (>= x y))
+(assert (<= x y))
+(check-sat)
diff --git a/regression/QF_UFLRA/incremental.smt2.expected.err b/regression/QF_UFLRA/incremental.smt2.expected.err
diff --git a/regression/QF_UFLRA/incremental.smt2.expected.out b/regression/QF_UFLRA/incremental.smt2.expected.out
@@ -0,0 +1 @@
+unsat