get values for nondet symbols

smowton · Feb 19, 2018 · 1ebec11 · 1ebec11
1 parent a827c77
commit 1ebec11
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -189,6 +189,15 @@ exprt smt2_convt::get(const exprt &expr) const
     if(it!=identifier_map.end())
       return it->second.value;
   }
+  else if(expr.id()==ID_nondet_symbol)
+  {
+    const irep_idt &id=to_nondet_symbol_expr(expr).get_identifier();
+
+    identifier_mapt::const_iterator it=identifier_map.find(id);
+
+    if(it!=identifier_map.end())
+      return it->second.value;
+  }
   else if(expr.id()==ID_member)
   {
     const member_exprt &member_expr=to_member_expr(expr);