From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 3 Jan 2022 17:35:13 +0000 (-0800)
Subject: Execute `(reset)` command in parse-only mode (#7862)
X-Git-Tag: cvc5-1.0.0~619
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0d69fdbe64e6191bf3e1dfbc1c471da9dbaa7cc;p=cvc5.git

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 ae4dc1e9c..218ab554d 100644
--- 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 e19ef2f7e..6bca782f1 100644
--- 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
index 000000000..26e92350a
--- /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)