diff options
Diffstat (limited to 'src/main/command_executor.cpp')
| -rw-r--r-- | src/main/command_executor.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 8188f247f..f08d9adde 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -204,7 +204,11 @@ bool solverInvoke(api::Solver* solver, cmd->toStream(ss); } - if (solver->getOptionInfo("parse-only").boolValue()) + // In parse-only mode, we do not invoke any of the commands except define-fun + // 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) { return true; } |