diffblue · kroening · Dec 18, 2024 · Dec 17, 2024
diff --git a/lib/cbmc b/lib/cbmc
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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));
+2 −5		src/goto-cc/armcc_mode.cpp
+1 −4		src/goto-cc/gcc_mode.cpp
+4 −4		src/goto-instrument/goto_instrument_parse_options.cpp
+4 −2		src/solvers/flattening/boolbv.cpp
+117 −16		src/solvers/smt2/smt2_conv.cpp
+7 −7		src/solvers/smt2/smt2_parser.cpp
+34 −0		src/util/bitvector_expr.cpp
+185 −1		src/util/bitvector_expr.h
+15 −0		src/util/bitvector_types.h
+12 −2		src/util/cmdline.cpp
+3 −0		src/util/cmdline.h
+66 −0		src/util/floatbv_expr.h
+2 −1		src/util/format_expr.cpp
+1 −0		src/util/irep_ids.def
+29 −0		src/util/std_expr.cpp
+125 −0		src/util/std_expr.h
+78 −0		unit/util/bitvector_expr.cpp
+2 −0		unit/util/module_dependencies.txt