Linux Driver Verification » BLAST

Okay, I think it's a bug with SMT formula parts caching.

In one of the competition drivers, we see that one of the "true" predicates was cached as (not (= S8 0)), which prevents useful blockset from being UNSAT.

Region of the first block 42:
bs_assert:
And [Primed(cb@ssl3_accept, cb@ssl3_accept0)  !=  0,
Primed(Primed(* (Primed(s@ssl3_accept, s@ssl3_accept0) ), * (s@ssl3_accept)0).info_callback, (* (s@ssl3_accept)).info_callback0)  !=  0,
-(Primed(Primed(* (Primed(s@ssl3_accept, s@ssl3_accept0) ), * (s@ssl3_accept)0).state, 2088_)) >  -8656,
true]
Blocks fetched so far:
bs_assert:
Primed(Primed(* (Primed(s@ssl3_accept, s@ssl3_accept0) ), * (s@ssl3_accept)0).debug, (* (s@ssl3_accept)).debug0) ==  0
SMT conv key ub_123!
bs_assert:
true       // this one (?) is cached as (not (= S8 0))
Adding end_cons:
bs_assert:
true
Asserting trace up to 161:
Calling SMT solver for conj of 4 predicates
( benchmark Blast_query_25989
:logic AUFLIA
:extrafuns((S32 Int ))
:extrafuns((S31 Int ))
:extrafuns((S33 Int ))
....
:formula (and true true  (not (= S8 0)) (= S8 0) (and true (not (= S7 0)) (not (= S70 0)) (> (~ S50) (~ 8656)) true  ))
)

The file is attached, the runtime options are

pblast.opt -alias bdd -cref -cldepth 3 -nomusts -debug -bddprint -lattice -include-lattice symb -stop-sep -merge bdd -skipnorm -ialias -iclos -nolabelmeanssafe file.i

Fixed in a73abb4 in competition branch.

The only reason for the useful blocksets to be SAT for now is that they're satisfiable with real numbers, and unsat with integers.

The problems with satisfiable useful block sets are gone.