Merge pull request #8997 from diffblue/fix/no-unary-bv-concat-smt2

SMT2: avoid emitting unary bitvector concat

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -1299,22 +1299,31 @@ void smt2_convt::convert_expr(const exprt &expr)
       "concatenation expression should have at least one operand",
       expr.id_string());
 
-    if(expr.operands().size() == 1)
+    // collect non-zero-width operands (zero-width not allowed by SMT-LIB)
+    exprt::operandst non_zero_width_ops;
+    for(const auto &op : expr.operands())
     {
-      flatten2bv(expr.operands().front());
+      if(!is_zero_width(op.type(), ns))
+        non_zero_width_ops.push_back(op);
     }
-    else // >= 2
+
+    DATA_INVARIANT(
+      !non_zero_width_ops.empty(),
+      "concatenation must have at least one non-zero-width operand");
+
+    if(non_zero_width_ops.size() == 1)
+    {
+      // unary concat is not valid SMT-LIB; emit the operand directly
+      flatten2bv(non_zero_width_ops.front());
+    }
+    else
     {
       out << "(concat";
 
-      for(const auto &op : expr.operands())
+      for(const auto &op : non_zero_width_ops)
       {
-        // drop zero-width operands, which are not allowed by SMT-LIB
-        if(!is_zero_width(op.type(), ns))
-        {
-          out << ' ';
-          flatten2bv(op);
-        }
+        out << ' ';
+        flatten2bv(op);
       }
 
       out << ')';

src/util/bitvector_expr.h

@@ -952,7 +952,8 @@ inline replication_exprt &to_replication_expr(exprt &expr)
 
 /// \brief Concatenation of bit-vector operands
 ///
-/// This expression takes any number of operands
+/// This expression takes any number of operands, including
+/// zero-width operands.
 /// The ordering of the operands is the same as in the SMT-LIB 2 standard,
 /// i.e., most-significant operands come first.
 class concatenation_exprt : public multi_ary_exprt

unit/solvers/smt2/smt2_conv.cpp

@@ -3,6 +3,7 @@
 /// \file
 /// Unit tests for smt2_convt
 
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -114,3 +115,18 @@ TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]")
       "(assert (not (= y (_ bv0 1))))");
   }
 }
+
+TEST_CASE(
+  "smt2_convt no unary concat for zero-width operand",
+  "[core][solvers][smt2]")
+{
+  unsignedbv_typet u8{8};
+  unsignedbv_typet u0{0};
+  symbol_exprt x{"x", u8};
+  symbol_exprt z{"z", u0};
+
+  // concat of a zero-width and a non-zero-width operand should emit
+  // the non-zero-width operand directly, not (concat x)
+  concatenation_exprt concat{{z, x}, u8};
+  REQUIRE(get_assert(equal_exprt{concat, x}) == "(assert (= x x))");
+}