diff --git a/lib/cbmc b/lib/cbmc
index d148ae6e8..15eb10ad9 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit d148ae6e880a3ef167bb71e9ed28169578899dce
+Subproject commit 15eb10ad9ddd3519ab533e4771ac26b6ee244f6e
diff --git a/regression/ebmc/elbtunnel/test.desc b/regression/ebmc/elbtunnel/test.desc
index a9b66bb49..6912c66fc 100644
--- a/regression/ebmc/elbtunnel/test.desc
+++ b/regression/ebmc/elbtunnel/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 elbtunnel.aig.smv
 --bound 12
 ^EXIT=10$
@@ -14,4 +14,3 @@ elbtunnel.aig.smv
 --
 ^warning: ignoring
 --
-The test fails in MacOS CI with Z3.
diff --git a/regression/smv/expressions/smv_toint1.desc b/regression/smv/expressions/smv_toint1.desc
index 805020b83..2f6f4482d 100644
--- a/regression/smv/expressions/smv_toint1.desc
+++ b/regression/smv/expressions/smv_toint1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-smt-backend
 smv_toint1.smv
 
 ^\[.*\] toint\(0\) = 0: PROVED .*$
diff --git a/regression/verilog/expressions/inside1.desc b/regression/verilog/expressions/inside1.desc
index 2b4f9eb87..303c1c2e5 100644
--- a/regression/verilog/expressions/inside1.desc
+++ b/regression/verilog/expressions/inside1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 inside1.sv
 
 ^\[.*\] always 2 inside \{1, 2, 3\}: PROVED .*$
diff --git a/regression/verilog/expressions/signing_cast1.desc b/regression/verilog/expressions/signing_cast1.desc
index 619d6bb2b..c6cef03f7 100644
--- a/regression/verilog/expressions/signing_cast1.desc
+++ b/regression/verilog/expressions/signing_cast1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 signing_cast1.sv
 --module main
 ^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED .*$
@@ -12,4 +12,3 @@ signing_cast1.sv
 --
 ^warning: ignoring
 --
-The width of the operand is not preserved.
diff --git a/src/ebmc/ebmc_solver_factory.cpp b/src/ebmc/ebmc_solver_factory.cpp
index fc20557a7..018311756 100644
--- a/src/ebmc/ebmc_solver_factory.cpp
+++ b/src/ebmc/ebmc_solver_factory.cpp
@@ -124,6 +124,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
             std::string("Generated by EBMC ") + EBMC_VERSION,
             "QF_AUFBV",
             smt2_solver.value(),
+            "", // solver binary
             message_handler)};
         }
       };
diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
index a98afa962..a2d7d1814 100644
--- a/src/trans-netlist/unwind_netlist.cpp
+++ b/src/trans-netlist/unwind_netlist.cpp
@@ -21,40 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*******************************************************************\
 
-Function: cnf_gate_and
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-// This is a copy of cnft::gate_and, which is protected.
-inline void cnf_gate_and(cnft &cnf, literalt a, literalt b, literalt o)
-{
-  // a*b=c <==> (a + o')( b + o')(a'+b'+o)
-  bvt lits(2);
-
-  lits[0] = pos(a);
-  lits[1] = neg(o);
-  cnf.lcnf(lits);
-
-  lits[0] = pos(b);
-  lits[1] = neg(o);
-  cnf.lcnf(lits);
-
-  lits.clear();
-  lits.reserve(3);
-  lits.push_back(neg(a));
-  lits.push_back(neg(b));
-  lits.push_back(pos(o));
-  cnf.lcnf(lits);
-}
-
-/*******************************************************************\
-
 Function: unwind
 
   Inputs:
@@ -102,7 +68,7 @@ void unwind(
       literalt la=bmc_map.translate(t, node.a);
       literalt lb=bmc_map.translate(t, node.b);
 
-      cnf_gate_and(solver, la, lb, timeframe[n].solver_literal);
+      solver.gate_and(la, lb, timeframe[n].solver_literal);
     }
   }