Bump CBMC dependency

kroening · kroening · commit 090d419ccb20 · 2024-12-17T16:43:21.000-08:00
diff --git 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
@@ -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));

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE`
`2`	`2`	`range_type1.smv`
`3`	`3`	`--bound 10`
`4`	`4`	`^EXIT=0$`