Adding test

Stevendeo · Dec 4, 2023 · 644f2e9 · 644f2e9
1 parent cdacde1
commit 644f2e9
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 0 deletions.
diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/tests/smtlib/testfile-push-pop2.dolmen.expected b/tests/smtlib/testfile-push-pop2.dolmen.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/smtlib/testfile-push-pop2.dolmen.smt2 b/tests/smtlib/testfile-push-pop2.dolmen.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(push 1)
+(assert (> x 0))
+(push 1)
+(pop 1)
+(pop 1)
+(assert (< x 0))
+(check-sat)