Skip to content

Commit c50d63e

Browse files
polgreenDaniel Kroening
authored and
Daniel Kroening
committed
get values for nondet symbols
1 parent f240f27 commit c50d63e

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/solvers/smt2/smt2_conv.cpp

+9
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,15 @@ exprt smt2_convt::get(const exprt &expr) const
189189
if(it!=identifier_map.end())
190190
return it->second.value;
191191
}
192+
else if(expr.id()==ID_nondet_symbol)
193+
{
194+
const irep_idt &id=to_nondet_symbol_expr(expr).get_identifier();
195+
196+
identifier_mapt::const_iterator it=identifier_map.find(id);
197+
198+
if(it!=identifier_map.end())
199+
return it->second.value;
200+
}
192201
else if(expr.id()==ID_member)
193202
{
194203
const member_exprt &member_expr=to_member_expr(expr);

0 commit comments

Comments
 (0)