SMT2: fix for encoding of range-typed symbols

src/solvers/smt2/smt2_conv.cpp

@@ -5458,7 +5458,22 @@ void smt2_convt::find_symbols(const exprt &expr)
         convert_type(expr.type());
       }
 
-      out << ")" << "\n";
+      out << ')' << '\n';
+
+      // We need an additional constraint for range-typed symbols,
+      // or otherwise we get satisfying assignments with values
+      // outside of the range when the size of the range isn't
+      // a power of two.
+      if(expr.type().id() == ID_range)
+      {
+        auto &range_type = to_integer_range_type(expr.type());
+        if(!is_power_of_two(range_type.size()))
+        {
+          out << "(assert (bvule " << smt2_identifier << ' ';
+          convert_expr(from_integer(range_type.to(), range_type));
+          out << "))\n"; // bvule, assert
+        }
+      }
     }
   }
   else if(expr.id() == ID_array_of)

src/util/arith_tools.cpp

@@ -202,6 +202,17 @@ std::size_t address_bits(const mp_integer &size)
   return result;
 }
 
+bool is_power_of_two(const mp_integer &n)
+{
+  mp_integer x;
+
+  for(x = 1; n > x; x *= 2)
+  {
+  }
+
+  return x == n;
+}
+
 /// A multi-precision implementation of the power operator.
 /// \par parameters: Two mp_integers, base and exponent
 /// \return One mp_integer with the value base^{exponent}

src/util/arith_tools.h

@@ -163,6 +163,8 @@ std::size_t address_bits(const mp_integer &size);
 
 mp_integer power(const mp_integer &base, const mp_integer &exponent);
 
+bool is_power_of_two(const mp_integer &);
+
 void mp_min(mp_integer &a, const mp_integer &b);
 void mp_max(mp_integer &a, const mp_integer &b);
 

unit/Makefile

@@ -142,6 +142,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/strings/string_refinement/string_refinement.cpp \
        solvers/strings/string_refinement/substitute_array_list.cpp \
        solvers/strings/string_refinement/union_find_replace.cpp \
+       util/arith_tools.cpp \
        util/bitvector_expr.cpp \
        util/case_expr.cpp \
        util/cmdline.cpp \

unit/solvers/smt2/smt2_conv.cpp

@@ -3,13 +3,17 @@
 /// \file
 /// Unit tests for smt2_convt
 
+#include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
 #include <solvers/smt2/smt2_conv.h>
+#include <solvers/smt2/smt2_dec.h>
 #include <testing-utils/use_catch.h>
 
 TEST_CASE(
@@ -130,3 +134,32 @@ TEST_CASE(
   concatenation_exprt concat{{z, x}, u8};
   REQUIRE(get_assert(equal_exprt{concat, x}) == "(assert (= x x))");
 }
+
+TEST_CASE("smt2_convt range encoding", "[core][solvers][smt2]")
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  null_message_handlert message_handler;
+  smt2_dect smt2_dec(
+    ns,
+    "unit test",
+    "",
+    "QF_AUFBV",
+    smt2_dect::solvert::Z3,
+    "",
+    message_handler);
+
+  GIVEN("An unsatisfiable formula over range-typed variables")
+  {
+    integer_range_typet range_type{0, 2}; // {0,...,2}
+    symbol_exprt a{"a", range_type};
+    smt2_dec << notequal_exprt{a, from_integer(0, range_type)};
+    smt2_dec << notequal_exprt{a, from_integer(1, range_type)};
+    smt2_dec << notequal_exprt{a, from_integer(2, range_type)};
+
+    THEN("the SMT2 solver says it's UNSAT")
+    {
+      REQUIRE(smt2_dec() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+}

unit/util/arith_tools.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Unit test for util/arith_tools.h
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <util/arith_tools.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("is_power_of_two", "[unit][util][arith_tools]")
+{
+  REQUIRE(!is_power_of_two(0));
+  REQUIRE(is_power_of_two(1));
+  REQUIRE(is_power_of_two(2));
+  REQUIRE(!is_power_of_two(3));
+  REQUIRE(is_power_of_two(4));
+}