diffblue · tautschnig · Nov 29, 2024 · Nov 29, 2024
diff --git a/lib/cbmc b/lib/cbmc
diff --git a/src/ebmc/ebmc_solver_factory.cpp b/src/ebmc/ebmc_solver_factory.cpp
@@ -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

diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.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())};
 }

diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.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
+1 −1		.github/workflows/coverage.yaml
+71 −0		.github/workflows/release-packages.yaml
+20 −0		CHANGELOG
+5 −5		doc/cprover-manual/memory-primitives.md
+3 −3		regression/cbmc/Pointer_difference2/test.desc
+1 −33		src/config.inc
+2 −1		src/goto-checker/solver_factory.cpp
+73 −0		src/goto-instrument/contracts/doc/user/contracts-assigns.md
+1 −1		src/libcprover-rust/Cargo.toml
+2 −33		src/solvers/flattening/bv_pointers.cpp
+2 −2		src/solvers/sat/satcheck.h
+21 −9		src/solvers/sat/satcheck_cadical.cpp
+25 −3		src/solvers/sat/satcheck_cadical.h
+8 −2		src/util/arith_tools.cpp
+35 −0		src/util/bitvector_expr.h
+5 −2		src/util/format_expr.cpp
+8 −0		src/util/mathematical_expr.cpp
+27 −11		src/util/mathematical_expr.h
+8 −7		src/util/simplify_expr.cpp
+2 −1		src/util/simplify_expr_class.h
+14 −5		src/util/simplify_expr_int.cpp
+5 −0		src/util/std_expr.h
+3 −3		unit/solvers/sat/satcheck_cadical.cpp
+1 −1		unit/util/format_expr.cpp
+17 −2		unit/util/simplify_expr.cpp