Skip to content

Commit 9909511

Browse files
committed
Make get_identifier use complete lowering chain
The previous lowering of enums alone prevents this from working as needed for structs.
1 parent 2561574 commit 9909511

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -355,7 +355,7 @@ smt2_incremental_decision_proceduret::get_identifier(const exprt &expr) const
355355
return expr_find_result->second;
356356

357357
// If that didn't yield any results, then try the lowered form.
358-
const exprt lowered_expr = lower_enum(expr, ns);
358+
const exprt lowered_expr = lower(expr);
359359
const auto lowered_handle_find_result =
360360
expression_handle_identifiers.find(lowered_expr);
361361
if(lowered_handle_find_result != expression_handle_identifiers.cend())
@@ -589,7 +589,7 @@ void smt2_incremental_decision_proceduret::define_object_properties()
589589
}
590590
}
591591

592-
exprt smt2_incremental_decision_proceduret::lower(exprt expression)
592+
exprt smt2_incremental_decision_proceduret::lower(exprt expression) const
593593
{
594594
const exprt lowered = struct_encoding.encode(
595595
lower_enum(lower_byte_operators(expression, ns), ns));

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ class smt2_incremental_decision_proceduret final
9797
/// Performs a combination of transformations which reduces the set of
9898
/// possible expression forms by expressing these in terms of the remaining
9999
/// language features.
100-
exprt lower(exprt expression);
100+
exprt lower(exprt expression) const;
101101
optionalt<smt_termt> get_identifier(const exprt &expr) const;
102102

103103
/// Namespace for looking up the expressions which symbol_exprts relate to.

0 commit comments

Comments
 (0)