WARNING: THIS SITE IS A MIRROR OF GITHUB.COM / IT CANNOT LOGIN OR REGISTER ACCOUNTS / THE CONTENTS ARE PROVIDED AS-IS / THIS SITE ASSUMES NO RESPONSIBILITY FOR ANY DISPLAYED CONTENT OR LINKS / IF YOU FOUND SOMETHING MAY NOT GOOD FOR EVERYONE, CONTACT ADMIN AT ilovescratch@foxmail.com
Skip to content

Commit 7727009

Browse files
thomasspriggsEnrico Steffinlongo
authored andcommitted
Add missing lowering of symbol values in new SMT backend
The previously missing lowering was causing invariant violations in `conver_expr_to_smt`.
1 parent a010865 commit 7727009

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -223,10 +223,11 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
223223
}
224224
else
225225
{
226-
if(push_dependencies_needed(symbol->value))
226+
const exprt lowered = lower(symbol->value);
227+
if(push_dependencies_needed(lowered))
227228
continue;
228229
const smt_define_function_commandt function{
229-
symbol->name, {}, convert_expr_to_smt(symbol->value)};
230+
symbol->name, {}, convert_expr_to_smt(lowered)};
230231
expression_identifiers.emplace(*symbol_expr, function.identifier());
231232
identifier_table.emplace(identifier, function.identifier());
232233
solver_process->send(function);

0 commit comments

Comments
 (0)