Merge pull request #854 from diffblue/cbmc-6.4.1

Bump CBMC to 6.4.1 release

Author: tautschnig

lib/cbmc

@@ -145,8 +145,8 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
       if(cmdline.isset("cadical"))
       {
 #ifdef SATCHECK_CADICAL
-        sat_solver =
-          std::unique_ptr<propt>(new satcheck_cadicalt{message_handler});
+        sat_solver = std::unique_ptr<propt>(
+          new satcheck_cadical_preprocessingt{message_handler});
 #else
         throw ebmc_errort() << "support for Cadical not configured";
 #endif

src/ebmc/ebmc_solver_factory.cpp

@@ -339,12 +339,12 @@ exprt aval_bval(const not_exprt &expr)
 exprt aval_bval(const power_exprt &expr)
 {
   PRECONDITION(is_four_valued(expr.type()));
-  PRECONDITION(is_aval_bval(expr.lhs()));
-  PRECONDITION(is_aval_bval(expr.rhs()));
+  PRECONDITION(is_aval_bval(expr.base()));
+  PRECONDITION(is_aval_bval(expr.exponent()));
 
-  auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
+  auto has_xz = or_exprt{::has_xz(expr.base()), ::has_xz(expr.exponent())};
   auto power_expr =
-    power_exprt{aval_underlying(expr.lhs()), aval_underlying(expr.rhs())};
+    power_exprt{aval_underlying(expr.base()), aval_underlying(expr.exponent())};
   auto x = make_x(expr.type());
   return if_exprt{has_xz, x, aval_bval_conversion(power_expr, x.type())};
 }

src/verilog/aval_bval_encoding.cpp

@@ -208,21 +208,21 @@ exprt verilog_lowering(exprt expr)
     else
     {
       DATA_INVARIANT(
-        power_expr.lhs().type() == power_expr.type(),
+        power_expr.base().type() == power_expr.type(),
         "power expression type consistency");
 
-      auto rhs_int = numeric_cast<std::size_t>(power_expr.rhs());
-      if(rhs_int.has_value())
+      auto exponent_int = numeric_cast<std::size_t>(power_expr.exponent());
+      if(exponent_int.has_value())
       {
-        if(*rhs_int == 0)
+        if(*exponent_int == 0)
           return from_integer(1, expr.type());
-        else if(*rhs_int == 1)
-          return power_expr.lhs();
+        else if(*exponent_int == 1)
+          return power_expr.base();
         else // >= 2
         {
-          auto factors = exprt::operandst{rhs_int.value(), power_expr.lhs()};
-          // would prefer appropriate mult_exprt constructor
-          return multi_ary_exprt{ID_mult, factors, expr.type()};
+          auto factors =
+            exprt::operandst{exponent_int.value(), power_expr.base()};
+          return mult_exprt{factors, expr.type()};
         }
       }
       else