[SMT-LIB] New SMT-LIB release for SMT-COMP 2011---includes fixes, additions

cok at frontiernet.net cok at frontiernet.net
Thu May 26 11:09:00 EDT 2011


Similarly in QF_LIA:

(* 512 (- 1)) is not linear according to the rules of the logic

- David

----- cok at frontiernet.net wrote:

> Morgan, Apologies if this is a duplicate report:
> 
> AUFLIA contains terms like (* 600 (+ (* rawhours__1 60)
> rawminutes__3))
> which are not linear by the rules specified in the logic (though this
> one is equivalent to  linear term)
> 
> - David


More information about the SMT-LIB mailing list