From e0d69fdbe64e6191bf3e1dfbc1c471da9dbaa7cc Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 3 Jan 2022 09:35:13 -0800 Subject: [PATCH] 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. --- src/main/command_executor.cpp | 3 ++- test/regress/CMakeLists.txt | 1 + .../regress/regress0/parser/issue7860-parse-only-reset.smt2 | 6 ++++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/parser/issue7860-parse-only-reset.smt2 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(cmd) == nullptr) + && dynamic_cast(cmd) == nullptr + && dynamic_cast(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) -- 2.30.2