Linux Driver Verification » BLAST

In development build of BLAST, usblp.o.i driver has several issues. One of them is a syntax error reported by CVC3. Here's the query that caused it:

SMT solver query: ( benchmark Blast_query_91                                                                               
:logic AUFLIA                                                                                                              
:extrafuns ((Address Int Int ))                                                                                            
:extrafuns ((BitAnd Int Int Int :assoc :comm))                                                                             
:extrafuns ((And Int Int Int :assoc :comm))                                                                                
:extrafuns ((offset Int Int Int ))                                                                                         
:extrafuns ((Foffset Int Int Int ))                                                                                        
:assumption (forall (?x Int) (?y Int) (?d1 Int) (implies (= (Foffset ?x ?d1) (Foffset ?y ?d1)) (= ?x ?y)))                 
:extrafuns((S16 Int ))
:extrafuns((S19 Int ))
:extrafuns((S9 Int ))
:extrafuns((S11 Int ))
:extrafuns((S25 Int ))
:extrafuns((S3 Int ))
:extrafuns((S27 Int ))
:extrafuns((S13 Int ))
:extrafuns((S30 Int ))
:extrafuns((S2 Int ))
:extrafuns((S7 Int ))
:extrafuns((S14 Int ))
:extrafuns((S31 Int ))
:extrafuns((S28 Int ))
:extrafuns((S24 Int ))
:extrafuns((S12 Int ))
:extrafuns((S15 Int ))
:extrafuns((S32 Int ))
:extrafuns((S6 Int ))
:extrafuns((S23 Int ))
:extrafuns((S4 Int ))
:extrafuns((S5 Int ))
:extrafuns((S21 Int ))
:extrafuns((S10 Int ))
:extrafuns((S29 Int ))
:extrafuns((S22 Int ))
:extrafuns((S17 Int ))
:extrafuns((S26 Int ))
:extrafuns((S1 Int ))
:extrafuns((S18 Int ))
:extrafuns((S8 Int ))
:extrafuns((S20 Int ))
:formula (and true true  true  (and true (= S2 (not (not (BitAnd S1 2048)))) (= S4 S3)) true  (not (= 512 1)) (not (= 512 2)) (not (= 512 4)) (not (= 512 8)) true  true  (= S6 S5) true  (and true (= S7 S6) (= S8 0) (= S10 (Address S9 )) (= S11 0) (= S12 0) (= S13 0)) true  true  true  (not (= 512 1)) (not (= 512 2)) (not (= 512 4)) (not (= 512 8)) true  true  (= S14 S5) true  (and true (= S15 512) (= S17 (Foffset S14 S16)) (= S18 1)) (not (= S15 1)) (not (= S15 2)) (not (= S15 4)) (not (= S15 8)) (= 0 0) true  true  (= S20 (Foffset S4 S19)) (= S21 0) (= S23 S22) true  (= S23 0) (= S24 0) (= S25 (~ 4)) (= S26 S25) true  true  (and true (= S27 S2) (= S28 S4)) (= S29 0) (= S30 (~ 19)) (= S31 S30) true  (= S32 (Foffset S4 S19)) (= S24 0) true  true )
)

block_at hits exceptionFailure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error")
bs_reset
Dumping Abstraction
Predicate Dependancy Table
Writing out .abs file: usblp.abs
Maximum #preds/loc: 0
Average #preds/loc: 0
Done writing .abs file
Exception raised :(Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error")
Stopping CSIsat process...
CSIsat stopped.
Stopping SMT solver process...
SMT solver stopped.
Ack! The gremlins again!: Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error")
Ack! The gremlins again!: Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error")
Fatal error: exception Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error")

Something should be fixed, I guess... The file is attached. Blast was run with:

pblast.opt  -predH 7 -craig 2 -ignoredupfn -nosserr -main ldv_main0 -L LDV_ERROR
-cldepth 0 -alias "" -cref -const  -smt -noinitialize  -bddprint 2>&1  -nomusts  -devdebug  2>&1  usblp.o.i