Execute `(reset)` command in parse-only mode (#7862)

This commit fixes an issue where `--parse-only` would not execute
`(reset)` commands, leading to issues with symbols being defined
multiple times.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index ae4dc1e9cd67f7a6316a057b1ba1be653c172b73..218ab554d74bde28b1cdd006c6d5fb4b8eb04d1c 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -207,7 +207,8 @@ bool solverInvoke(api::Solver* solver,
   // commands. We invoke define-fun commands because they add function names
   // to the symbol table.
   if (solver->getOptionInfo("parse-only").boolValue()
-      && dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr)
+      && dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr
+      && dynamic_cast<ResetCommand*>(cmd) == nullptr)
   {
     return true;
   }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e19ef2f7eef9386121dd1a090a978456f1628b50..6bca782f13b256b9af3dce6367cb18309a98fd27 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -810,6 +810,7 @@ set(regress_0_tests
   regress0/parser/issue5163.smt2
   regress0/parser/issue6908-get-value-uc.smt2
   regress0/parser/issue7274.smt2
+  regress0/parser/issue7860-parse-only-reset.smt2
   regress0/parser/linear_arithmetic_err1.smt2
   regress0/parser/linear_arithmetic_err2.smt2
   regress0/parser/linear_arithmetic_err3.smt2

diff --git a/test/regress/regress0/parser/issue7860-parse-only-reset.smt2 b/test/regress/regress0/parser/issue7860-parse-only-reset.smt2
new file mode 100644 (file)
index 0000000..26e9235
--- /dev/null
+++ b/test/regress/regress0/parser/issue7860-parse-only-reset.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --parse-only
+; EXIT: 0
+(set-logic ALL)
+(reset)
+(set-logic QF_UF)
+(declare-sort U 0)