Simplify __CPROVER_{r,w,rw}_ok expansion

When simplification is enabled, goto_check should produce simplified
expressions only.

Author: tautschnig

regression/cbmc/r_w_ok9/simplify.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+--
+false ∨
+∨ false
+--
+__CPROVER_{r,w,rw}_ok must be rewritten everywhere, and the resulting expression
+should be simplified (and, therefore, not contain "false" in a disjunction).

regression/validate-trace-xml-schema/check.py

@@ -25,6 +25,7 @@
     ['integer-assignments1', 'integer-typecheck.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
+    ['r_w_ok9', 'simplify.desc'],
     ['reachability-slice-interproc2', 'test.desc'],
     # this one wants show-properties instead producing a trace
     ['show_properties1', 'test.desc'],

src/analyses/goto_check_c.cpp

@@ -1918,7 +1918,10 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
     for(const auto &c : conditions)
       conjuncts.push_back(c.assertion);
 
-    return conjunction(conjuncts);
+    exprt c = conjunction(conjuncts);
+    if(enable_simplify)
+      simplify(c, ns);
+    return c;
   }
   else if(modified)
     return std::move(expr);