SMT2 back-end: ite-conversion must uphold type consistency

WITH expressions in an ite expression could previously trigger
one-sided expression flattening.

Author: tautschnig

regression/contracts-dfcc/array_struct_smt-02/main.c

@@ -0,0 +1,24 @@
+typedef struct
+{
+  int coeffs[1];
+} mld_poly;
+
+typedef struct
+{
+  mld_poly vec[1];
+} mld_polyveck;
+
+int main()
+{
+  mld_polyveck h;
+
+  // clang-format off
+  for(unsigned int i = 0; i < 1; ++i)
+    __CPROVER_loop_invariant(i <= 1)
+  {
+    h.vec[i].coeffs[0] = 1;
+  }
+  // clang-format on
+
+  return 0;
+}

regression/contracts-dfcc/array_struct_smt-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts _ --cprover-smt2
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Make sure the SMT back-end produces valid SMT2 when structs and arrays are
+nested in each other.

src/solvers/smt2/smt2_conv.cpp

@@ -1407,9 +1407,35 @@ void smt2_convt::convert_expr(const exprt &expr)
     out << "(ite ";
     convert_expr(if_expr.cond());
     out << " ";
-    convert_expr(if_expr.true_case());
+    if(
+      expr.type().id() == ID_array && !use_array_theory(if_expr.true_case()) &&
+      use_array_theory(if_expr.false_case()))
+    {
+      unflatten(wheret::BEGIN, expr.type());
+
+      convert_expr(if_expr.true_case());
+
+      unflatten(wheret::END, expr.type());
+    }
+    else
+    {
+      convert_expr(if_expr.true_case());
+    }
     out << " ";
-    convert_expr(if_expr.false_case());
+    if(
+      expr.type().id() == ID_array && use_array_theory(if_expr.true_case()) &&
+      !use_array_theory(if_expr.false_case()))
+    {
+      unflatten(wheret::BEGIN, expr.type());
+
+      convert_expr(if_expr.false_case());
+
+      unflatten(wheret::END, expr.type());
+    }
+    else
+    {
+      convert_expr(if_expr.false_case());
+    }
     out << ")";
   }
   else if(expr.id()==ID_and ||