Skip to content

Commit cf1fa4f

Browse files
committed
bump CBMC dependency to release 6.8.0
1 parent 4197882 commit cf1fa4f

File tree

6 files changed

+6
-7
lines changed

6 files changed

+6
-7
lines changed

lib/cbmc

Submodule cbmc updated 1342 files

regression/ebmc/elbtunnel/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
elbtunnel.aig.smv
33
--bound 12
44
^EXIT=10$
@@ -14,4 +14,3 @@ elbtunnel.aig.smv
1414
--
1515
^warning: ignoring
1616
--
17-
The test fails in MacOS CI with Z3.

regression/smv/expressions/smv_toint1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE broken-smt-backend
22
smv_toint1.smv
33

44
^\[.*\] toint\(0\) = 0: PROVED .*$

regression/verilog/expressions/inside1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
inside1.sv
33

44
^\[.*\] always 2 inside \{1, 2, 3\}: PROVED .*$

regression/verilog/expressions/signing_cast1.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
signing_cast1.sv
33
--module main
44
^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED .*$
@@ -12,4 +12,3 @@ signing_cast1.sv
1212
--
1313
^warning: ignoring
1414
--
15-
The width of the operand is not preserved.

src/ebmc/ebmc_solver_factory.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
124124
std::string("Generated by EBMC ") + EBMC_VERSION,
125125
"QF_AUFBV",
126126
smt2_solver.value(),
127+
"", // solver binary
127128
message_handler)};
128129
}
129130
};

0 commit comments

Comments
 (0)