fix for nondeterministic structs

Author: kroening

regression/cprover/function_calls/call_no_body2.desc

@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 call_no_body2.c
 --text
 ^EXIT=0$
 ^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S22-0\]\)$
 --

regression/cprover/structs/nondet_struct1.c

@@ -8,4 +8,5 @@ struct S nondet_S();
 int main()
 {
   s = nondet_S();
+  return 0;
 }

regression/cprover/structs/nondet_struct1.desc

@@ -1,6 +1,7 @@
-KNOWNBUG
+CORE
 nondet_struct1.c
 --text
 ^EXIT=0$
 ^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞\.❝x❞:=nondet::S21-0\]\[❝s❞\.❝y❞:=nondet::S21-1\]\)$
 --

src/cprover/state_encoding.cpp

@@ -292,6 +292,11 @@ exprt state_encodingt::evaluate_expr_rec(
       evaluate_expr_rec(loc, state, is_cstring_expr.op(), bound_symbols);
     return binary_predicate_exprt(state, ID_state_is_cstring, pointer);
   }
+  else if(what.id() == ID_side_effect)
+  {
+    // leave as is
+    return what;
+  }
   else
   {
     exprt tmp = what;
@@ -436,6 +441,13 @@ exprt state_encodingt::assignment_constraint_rec(
 
       if(rhs.id() == ID_struct)
         rhs_member = simplify_expr(rhs_member, ns);
+      else if(
+        rhs.id() == ID_side_effect &&
+        to_side_effect_expr(rhs).get_statement() == ID_nondet)
+      {
+        rhs_member =
+          side_effect_expr_nondett(rhs_member.type(), rhs.source_location());
+      }
 
       new_state = assignment_constraint_rec(
         loc, new_state, lhs_member, rhs_member, nondet_symbols);