Merge pull request #7299 from tautschnig/bugfixes/smt-union-flatten

SMT back-end: use_array_theory compatibility with unions

Author: tautschnig

regression/cbmc/bounds_check1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE thorough-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$
@@ -12,3 +12,6 @@ payload\[\(.*\)[kl]2\]: FAILURE
 \[\(.*\)i\]: FAILURE
 dest\[\(.*\)j\]: FAILURE
 payload\[\(.*\)[kl]\]: FAILURE
+--
+Appears to take Z3 more than 10 minutes to solve, and approximately 500 seconds
+when using the in-tree SMT solver.

regression/cbmc/union/union_member.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 union_member.c
 
 ^EXIT=10$
@@ -8,6 +8,3 @@ union_member.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
---
-This fails when using the SMT backend with Z3 with the error message
-"select requires 1 arguments, but was provided with 2 arguments"

regression/cbmc/union/union_update.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend
+CORE
 union_update.c
 
 ^EXIT=10$
@@ -8,6 +8,3 @@ union_update.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
---
-This fails when using the SMT backend with Z3 with the error message
-"store expects the first argument sort to be an array".

src/solvers/smt2/smt2_conv.cpp

@@ -5459,20 +5459,18 @@ bool smt2_convt::use_array_theory(const exprt &expr)
   const typet &type = expr.type();
   PRECONDITION(type.id()==ID_array);
 
-  if(use_datatypes)
+  // a union is always flattened; else always use array theory when we have
+  // datatypes
+  if(expr.id() == ID_with)
+    return use_array_theory(to_with_expr(expr).old());
+  else if(auto member = expr_try_dynamic_cast<member_exprt>(expr))
   {
-    return true; // always use array theory when we have datatypes
+    // arrays inside structs get flattened, unless we have datatypes
+    return use_datatypes && member->compound().type().id() != ID_union &&
+           member->compound().type().id() != ID_union_tag;
   }
   else
-  {
-    // arrays inside structs or unions get flattened
-    if(expr.id()==ID_with)
-      return use_array_theory(to_with_expr(expr).old());
-    else if(expr.id()==ID_member)
-      return false;
-    else
-      return true;
-  }
+    return true;
 }
 
 void smt2_convt::convert_type(const typet &type)