Solving time problem

[Rico1900]

When verifying a Verilog design using ebmc with large bounds, it takes long time to complete the verification. However, if I output the SMT formulas and solve the formulas using z3 command, it takes instant to solve the problem. In my opinion, these two approaches should consume similar time since encoding Verilog and properties as SMT formulas is fast. Here's the procedure to reproduce the phenomenon.

hw-cbmc version: main-latest

Verilog code:

module main (clk);
input clk;
reg [2500:0] a,b;	
	
initial a = 1;
initial b = 0;

always @ (posedge clock) begin
	if (a<100) 
	   a<=b+a;
	b <=a;
end

endmodule

ebmc verification command:

ebmc example.v --top main --bound 1000 -p "a < 200" --z3

This command takes almost 110 seconds on my machine.

ebmc export SMT formula:

ebmc example.v --top main --bound 1000 -p "a < 200" --smt2 | awk '!/^Parsing|^Converting|^Type-checking|^Generating|^Properties/ END {print "(check-sat)"}' > formula.smt

This command exports formulas in SMT lib 2 format. Then I tried to solve the formulas with z3:

z3 -model -smt2 formula.smt -st

And it outputs the following instantly:

unsat
(:max-memory   21.89
 :memory       20.90
 :num-allocs   2516964
 :rlimit-count 56060
 :time         0.01
 :total-time   0.04)

In model checking approach, unsat means that the property is proved up to the bound, right? So, my question is that why the time consumptions of these two approaches differ so greatly?

[kroening]

The difference in performance here is indeed extreme. It arises from the fact that EBMC uses (check-sat-assuming ...) when solving, and (assert ...) (check-sat) when exporting. Z3 seems to perform much better when using the latter.

[kroening]

Small data point: CVC5 1.2.0 does not suffer from this, and solves both instances quickly.