diff --git a/lib/cbmc b/lib/cbmc
index c902db34b..fb2847509 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit c902db34beb113815f151c4d1f635e745ac79c0c
+Subproject commit fb284750934f5830501990d54c1d8118c7af0d3d
diff --git a/regression/ebmc/range_type/range_type1.desc b/regression/ebmc/range_type/range_type1.desc
index 6a72be6c8..cd48ef65c 100644
--- a/regression/ebmc/range_type/range_type1.desc
+++ b/regression/ebmc/range_type/range_type1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 range_type1.smv
 --bound 10
 ^EXIT=0$
diff --git a/regression/ebmc/range_type/range_type4.desc b/regression/ebmc/range_type/range_type4.desc
index 8c4b05d8f..c36e4105c 100644
--- a/regression/ebmc/range_type/range_type4.desc
+++ b/regression/ebmc/range_type/range_type4.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 range_type4.smv
 --bound 10
 ^EXIT=0$
diff --git a/regression/ebmc/traces/disjunction1.desc b/regression/ebmc/traces/disjunction1.desc
index c5b16109f..979937e30 100644
--- a/regression/ebmc/traces/disjunction1.desc
+++ b/regression/ebmc/traces/disjunction1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 disjunction1.smv
 --bound 20 --numbered-trace
 ^\[spec1\] G \(X FALSE \| X X FALSE\): REFUTED$
diff --git a/regression/smv/CTL/smv_ctlspec_F1.desc b/regression/smv/CTL/smv_ctlspec_F1.desc
index 3fac6aacc..91236eccb 100644
--- a/regression/smv/CTL/smv_ctlspec_F1.desc
+++ b/regression/smv/CTL/smv_ctlspec_F1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ctlspec_F1.smv
 --bound 10
 ^\[.*\] AF x = 0: REFUTED$
diff --git a/regression/smv/CTL/smv_ctlspec_G1.desc b/regression/smv/CTL/smv_ctlspec_G1.desc
index 291451aeb..e2604b804 100644
--- a/regression/smv/CTL/smv_ctlspec_G1.desc
+++ b/regression/smv/CTL/smv_ctlspec_G1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ctlspec_G1.smv
 --bound 10
 ^\[.*\] AG x != 5: PROVED up to bound 10$
diff --git a/regression/smv/LTL/smv_ltlspec6.desc b/regression/smv/LTL/smv_ltlspec6.desc
index cbb97eb47..b2736a00d 100644
--- a/regression/smv/LTL/smv_ltlspec6.desc
+++ b/regression/smv/LTL/smv_ltlspec6.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec6.smv
 
 ^EXIT=0$
diff --git a/regression/smv/LTL/smv_ltlspec_F1.desc b/regression/smv/LTL/smv_ltlspec_F1.desc
index e716671d2..6b072e0a7 100644
--- a/regression/smv/LTL/smv_ltlspec_F1.desc
+++ b/regression/smv/LTL/smv_ltlspec_F1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_F1.smv
 --bound 10
 ^EXIT=10$
diff --git a/regression/smv/LTL/smv_ltlspec_F2.desc b/regression/smv/LTL/smv_ltlspec_F2.desc
index 7b672c256..8fe3683c5 100644
--- a/regression/smv/LTL/smv_ltlspec_F2.desc
+++ b/regression/smv/LTL/smv_ltlspec_F2.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_F2.smv
 --bound 10
 ^EXIT=10$
diff --git a/regression/smv/LTL/smv_ltlspec_F3.desc b/regression/smv/LTL/smv_ltlspec_F3.desc
index d4ff52613..db908e9f8 100644
--- a/regression/smv/LTL/smv_ltlspec_F3.desc
+++ b/regression/smv/LTL/smv_ltlspec_F3.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_F3.smv
 --bound 10 --numbered-trace
 ^\[.*\] F x = 0: REFUTED$
diff --git a/regression/smv/LTL/smv_ltlspec_G1.desc b/regression/smv/LTL/smv_ltlspec_G1.desc
index f36e383c8..5946bb2a5 100644
--- a/regression/smv/LTL/smv_ltlspec_G1.desc
+++ b/regression/smv/LTL/smv_ltlspec_G1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_G1.smv
 --bound 10
 ^EXIT=10$
diff --git a/regression/smv/LTL/smv_ltlspec_G2.desc b/regression/smv/LTL/smv_ltlspec_G2.desc
index e32cce870..cc411baaa 100644
--- a/regression/smv/LTL/smv_ltlspec_G2.desc
+++ b/regression/smv/LTL/smv_ltlspec_G2.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_G2.smv
 --bound 10
 ^EXIT=10$
diff --git a/regression/smv/LTL/smv_ltlspec_G3.desc b/regression/smv/LTL/smv_ltlspec_G3.desc
index 71e3a27a4..5d4a558a6 100644
--- a/regression/smv/LTL/smv_ltlspec_G3.desc
+++ b/regression/smv/LTL/smv_ltlspec_G3.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_G3.smv
 --bound 10 --numbered-trace
 ^\[.*\] G X x != 3: REFUTED$
diff --git a/regression/smv/LTL/smv_ltlspec_R1.desc b/regression/smv/LTL/smv_ltlspec_R1.desc
index 4d84bdbfc..3233a406a 100644
--- a/regression/smv/LTL/smv_ltlspec_R1.desc
+++ b/regression/smv/LTL/smv_ltlspec_R1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_R1.smv
 --bound 10
 ^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$
diff --git a/regression/smv/LTL/smv_ltlspec_R3.desc b/regression/smv/LTL/smv_ltlspec_R3.desc
index 7b5d9356e..55688211b 100644
--- a/regression/smv/LTL/smv_ltlspec_R3.desc
+++ b/regression/smv/LTL/smv_ltlspec_R3.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_R3.smv
 --bound 1
 ^\[.*\] FALSE R x != 3: PROVED up to bound 1$
diff --git a/regression/smv/LTL/smv_ltlspec_R4.desc b/regression/smv/LTL/smv_ltlspec_R4.desc
index fe268f524..7671d6989 100644
--- a/regression/smv/LTL/smv_ltlspec_R4.desc
+++ b/regression/smv/LTL/smv_ltlspec_R4.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_R4.smv
 --bound 10
 ^\[.*\] FALSE R x != 0: PROVED up to bound 10$
diff --git a/regression/smv/LTL/smv_ltlspec_U1.desc b/regression/smv/LTL/smv_ltlspec_U1.desc
index febf0d1f4..e59b642c5 100644
--- a/regression/smv/LTL/smv_ltlspec_U1.desc
+++ b/regression/smv/LTL/smv_ltlspec_U1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_U1.smv
 --bound 3
 \[.*\] TRUE U x = 3: PROVED up to bound 3$
diff --git a/regression/smv/LTL/smv_ltlspec_U2.desc b/regression/smv/LTL/smv_ltlspec_U2.desc
index ec6a58f8d..09c3f8db0 100644
--- a/regression/smv/LTL/smv_ltlspec_U2.desc
+++ b/regression/smv/LTL/smv_ltlspec_U2.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_ltlspec_U2.smv
 --bound 10 --numbered-trace
 ^\[.*\] TRUE U x = 0: REFUTED$
diff --git a/regression/smv/expressions/smv_if1.desc b/regression/smv/expressions/smv_if1.desc
index 3ee995e40..7bc5966ae 100644
--- a/regression/smv/expressions/smv_if1.desc
+++ b/regression/smv/expressions/smv_if1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 smv_if1.smv
 
 ^EXIT=0$
diff --git a/regression/verilog/assignments/assignment-to-concatenation1.desc b/regression/verilog/assignments/assignment-to-concatenation1.desc
index 673825e1d..7a8281593 100644
--- a/regression/verilog/assignments/assignment-to-concatenation1.desc
+++ b/regression/verilog/assignments/assignment-to-concatenation1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 assignment-to-concatenation1.v
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/assignments/assignment-to-index1.desc b/regression/verilog/assignments/assignment-to-index1.desc
index a1f0805c5..37d4c7250 100644
--- a/regression/verilog/assignments/assignment-to-index1.desc
+++ b/regression/verilog/assignments/assignment-to-index1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 assignment-to-index1.v
 --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/generate/generate-for2.desc b/regression/verilog/generate/generate-for2.desc
index ec4829241..168a17e6e 100644
--- a/regression/verilog/generate/generate-for2.desc
+++ b/regression/verilog/generate/generate-for2.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 generate-for2.v
 --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/generate/generate-reg1.desc b/regression/verilog/generate/generate-reg1.desc
index 01c703bc9..60a3c80a2 100644
--- a/regression/verilog/generate/generate-reg1.desc
+++ b/regression/verilog/generate/generate-reg1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 generate-reg1.v
 --module main --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/generate1/test.desc b/regression/verilog/generate1/test.desc
index 415cc5c10..6a3d0fa20 100644
--- a/regression/verilog/generate1/test.desc
+++ b/regression/verilog/generate1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.v
 --module main --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/multiple_assign1/test.desc b/regression/verilog/multiple_assign1/test.desc
index 415cc5c10..6a3d0fa20 100644
--- a/regression/verilog/multiple_assign1/test.desc
+++ b/regression/verilog/multiple_assign1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.v
 --module main --bound 1
 ^EXIT=0$
diff --git a/regression/verilog/part-select/indexed-part-select1.desc b/regression/verilog/part-select/indexed-part-select1.desc
index 39181c2be..5990bdc0d 100644
--- a/regression/verilog/part-select/indexed-part-select1.desc
+++ b/regression/verilog/part-select/indexed-part-select1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 indexed-part-select1.sv
 --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/primitive_gates/nand1.desc b/regression/verilog/primitive_gates/nand1.desc
index 2b5bbef22..da1db3f8c 100644
--- a/regression/verilog/primitive_gates/nand1.desc
+++ b/regression/verilog/primitive_gates/nand1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 nand1.sv
 --bound 0
 ^EXIT=0$
diff --git a/regression/verilog/primitive_gates/xnor3.desc b/regression/verilog/primitive_gates/xnor3.desc
index c0221a595..7f4836cde 100644
--- a/regression/verilog/primitive_gates/xnor3.desc
+++ b/regression/verilog/primitive_gates/xnor3.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 xnor3.sv
 --bound 0
 ^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED up to bound 0$
diff --git a/regression/verilog/system-functions/low1.desc b/regression/verilog/system-functions/low1.desc
index b345c1083..81145fc4a 100644
--- a/regression/verilog/system-functions/low1.desc
+++ b/regression/verilog/system-functions/low1.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 low1.sv
 --module main --bound 0
 ^EXIT=0$
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index 5f673cfe8..0997641e4 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -275,8 +275,7 @@ int ebmc_parse_optionst::doit()
         netlistt netlist;
         if(ebmc_base.make_netlist(netlist))
           return 1;
-        auto filename =
-          cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
+        auto filename = cmdline.value_opt("outfile").value_or("-");
         output_filet outfile{filename};
         outfile.stream() << "digraph netlist {\n";
         netlist.output_dot(outfile.stream());
@@ -289,8 +288,7 @@ int ebmc_parse_optionst::doit()
         netlistt netlist;
         if(ebmc_base.make_netlist(netlist))
           return 1;
-        auto filename =
-          cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-";
+        auto filename = cmdline.value_opt("outfile").value_or("-");
         output_filet outfile{filename};
         outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
         outfile.stream() << "-- Generated from "
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 506c49351..939717f76 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -238,7 +238,6 @@ IREP_ID_ONE(verilog_time)
 IREP_ID_ONE(verilog_iff)
 IREP_ID_ONE(verilog_implies)
 IREP_ID_ONE(offset)
-IREP_ID_ONE(xnor)
 IREP_ID_ONE(specify)
 IREP_ID_ONE(x)
 IREP_ID_ONE(verilog_empty_item)
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index 94d1c6b94..646efcb4d 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/src/verilog/verilog_synthesis.cpp
@@ -1572,11 +1572,9 @@ void verilog_synthesist::synth_module_instance_builtin(
       exprt op;
 
       if(instance.type().id() == ID_bool)
-        op = not_exprt{
-          multi_ary_exprt{ID_xor, std::move(operands), instance.type()}};
+        op = not_exprt{xor_exprt{std::move(operands)}};
       else
-        op = bitnot_exprt{
-          multi_ary_exprt{ID_bitxor, std::move(operands), instance.type()}};
+        op = bitnot_exprt{bitxor_exprt{std::move(operands), instance.type()}};
 
       equal_exprt constraint{output, std::move(op)};
       trans.invar().add_to_operands(std::move(constraint));