[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