simplify r_ok

Author: kroening

regression/cprover/safety/r_ok2.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 r_ok2.c
 --no-inline --safety
 ^EXIT=10$

src/cprover/simplify_state_expr.cpp

@@ -208,11 +208,11 @@ exprt simplify_ok_expr(
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   const namespacet &ns)
 {
-#if 0
-  const auto &state = src.op0();
-  const auto &pointer = src.op1();
-  const auto &size = src.op2();
+  auto &state = src.op0();
+  //auto &pointer = src.op1();
+  //auto &size = src.op2();
 
+#if 0
   // rewrite X_ok(p, s)
   //  --> live_object(p) ∧ offset(p)≥0 ∧ offset(p)+s≤object_size(p)
   auto live_object =
@@ -233,21 +233,17 @@ exprt simplify_ok_expr(
     plus_exprt(offset_simplified, size_casted), ID_le, object_size_simplified);
 
   return and_exprt(live_object_simplified, lower, upper);
-#else
-  return src;
 #endif
 
-#if 0
   // A store does not affect the result.
   // X_ok(ς[A:=V]), A, S) --> X_ok(ς, A, S)
-  if(src.op0().id() == ID_update_state)
+  if(state.id() == ID_update_state)
   {
-    src.op0() = to_update_state_expr(src.op0()).state();
+    state = to_update_state_expr(state).state();
     return std::move(src);
   }
 
   return src;
-#endif
 }
 
 #if 0