From 3a2fd5259107fc2cf24c27c5c78a9b929e3ecdf4 Mon Sep 17 00:00:00 2001
From: Steven de Oliveira <de.oliveira.steven@gmail.com>
Date: Mon, 2 Oct 2023 14:17:41 +0200
Subject: [PATCH] Adding tests

---
 tests/dune.inc                              | 587 ++++++++++++++++++++
 tests/smtlib/testfile-exit.dolmen.expected  |   2 +
 tests/smtlib/testfile-exit.dolmen.smt2      |   4 +
 tests/smtlib/testfile-exit.expected         |   2 +
 tests/smtlib/testfile-exit.smt2             |   4 +
 tests/smtlib/testfile-reset.dolmen.expected |   4 +
 tests/smtlib/testfile-reset.dolmen.smt2     |   8 +
 tests/smtlib/testfile-reset.expected        |   4 +
 tests/smtlib/testfile-reset.smt2            |   8 +
 9 files changed, 623 insertions(+)
 create mode 100644 tests/smtlib/testfile-exit.dolmen.expected
 create mode 100644 tests/smtlib/testfile-exit.dolmen.smt2
 create mode 100644 tests/smtlib/testfile-exit.expected
 create mode 100644 tests/smtlib/testfile-exit.smt2
 create mode 100644 tests/smtlib/testfile-reset.dolmen.expected
 create mode 100644 tests/smtlib/testfile-reset.dolmen.smt2
 create mode 100644 tests/smtlib/testfile-reset.expected
 create mode 100644 tests/smtlib/testfile-reset.smt2

diff --git a/tests/dune.inc b/tests/dune.inc
index fa7abd32d8..5671c652c9 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -203151,6 +203151,593 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir smtlib
+  (rule
+   (target testfile-reset_ci_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps testfile-reset_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-reset_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-reset_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-reset_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-reset_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-reset_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-reset_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target testfile-reset_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (deps testfile-reset_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target testfile-reset_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps testfile-reset_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-reset_cdcl.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (deps testfile-reset_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_cdcl.output)))
+  (rule
+   (target testfile-reset_tableaux_cdcl.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (deps testfile-reset_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_tableaux_cdcl.output)))
+  (rule
+   (target testfile-reset_tableaux.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (deps testfile-reset_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_tableaux.output)))
+  (rule
+   (target testfile-reset_legacy.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend legacy
+             %{input})))))))
+  (rule
+   (deps testfile-reset_legacy.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_legacy.output)))
+  (rule
+   (target testfile-reset_dolmen.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-reset_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_dolmen.output)))
+  (rule
+   (target testfile-reset_fpa.output)
+   (deps (:input testfile-reset.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (deps testfile-reset_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.expected testfile-reset_fpa.output)))
+  (rule
+   (target testfile-reset.dolmen_dolmen.output)
+   (deps (:input testfile-reset.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-reset.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-reset.dolmen.expected testfile-reset.dolmen_dolmen.output)))
+  (rule
+   (target testfile-exit_ci_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps testfile-exit_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-exit_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-exit_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-exit_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-exit_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target testfile-exit_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps testfile-exit_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target testfile-exit_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (deps testfile-exit_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target testfile-exit_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps testfile-exit_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target testfile-exit_cdcl.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (deps testfile-exit_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_cdcl.output)))
+  (rule
+   (target testfile-exit_tableaux_cdcl.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (deps testfile-exit_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_tableaux_cdcl.output)))
+  (rule
+   (target testfile-exit_tableaux.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (deps testfile-exit_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_tableaux.output)))
+  (rule
+   (target testfile-exit_legacy.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend legacy
+             %{input})))))))
+  (rule
+   (deps testfile-exit_legacy.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_legacy.output)))
+  (rule
+   (target testfile-exit_dolmen.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-exit_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_dolmen.output)))
+  (rule
+   (target testfile-exit_fpa.output)
+   (deps (:input testfile-exit.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (deps testfile-exit_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.expected testfile-exit_fpa.output)))
+  (rule
+   (target testfile-exit.dolmen_dolmen.output)
+   (deps (:input testfile-exit.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-exit.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-exit.dolmen.expected testfile-exit.dolmen_dolmen.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir sum
   (rule
diff --git a/tests/smtlib/testfile-exit.dolmen.expected b/tests/smtlib/testfile-exit.dolmen.expected
new file mode 100644
index 0000000000..a6e005255c
--- /dev/null
+++ b/tests/smtlib/testfile-exit.dolmen.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/smtlib/testfile-exit.dolmen.smt2 b/tests/smtlib/testfile-exit.dolmen.smt2
new file mode 100644
index 0000000000..135ade6d3a
--- /dev/null
+++ b/tests/smtlib/testfile-exit.dolmen.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(check-sat)
+(exit)
+(check-sat)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-exit.expected b/tests/smtlib/testfile-exit.expected
new file mode 100644
index 0000000000..a6e005255c
--- /dev/null
+++ b/tests/smtlib/testfile-exit.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/smtlib/testfile-exit.smt2 b/tests/smtlib/testfile-exit.smt2
new file mode 100644
index 0000000000..135ade6d3a
--- /dev/null
+++ b/tests/smtlib/testfile-exit.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(check-sat)
+(exit)
+(check-sat)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-reset.dolmen.expected b/tests/smtlib/testfile-reset.dolmen.expected
new file mode 100644
index 0000000000..76a9b3e2dd
--- /dev/null
+++ b/tests/smtlib/testfile-reset.dolmen.expected
@@ -0,0 +1,4 @@
+
+unsat
+
+unknown
diff --git a/tests/smtlib/testfile-reset.dolmen.smt2 b/tests/smtlib/testfile-reset.dolmen.smt2
new file mode 100644
index 0000000000..101715c147
--- /dev/null
+++ b/tests/smtlib/testfile-reset.dolmen.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(declare-const b Bool)
+
+(assert (and b (not b)))
+(check-sat)
+(reset)
+(check-sat)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-reset.expected b/tests/smtlib/testfile-reset.expected
new file mode 100644
index 0000000000..76a9b3e2dd
--- /dev/null
+++ b/tests/smtlib/testfile-reset.expected
@@ -0,0 +1,4 @@
+
+unsat
+
+unknown
diff --git a/tests/smtlib/testfile-reset.smt2 b/tests/smtlib/testfile-reset.smt2
new file mode 100644
index 0000000000..101715c147
--- /dev/null
+++ b/tests/smtlib/testfile-reset.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(declare-const b Bool)
+
+(assert (and b (not b)))
+(check-sat)
+(reset)
+(check-sat)
\ No newline at end of file