Parsing smtlib v2.0

50 views

Skip to first unread message

Sebastian Junges

unread,

Apr 12, 2012, 4:41:50 AM4/12/12

to opensmt

Hi,

while using OpenSMT we stumbled upon some misbehaviour when parsing
decimal values in OpenSMT from the smtlib 2.0 format.

We were able to find a small example which clearifies where the error
comes from. With the following input, OpenSMT returned unsat, since
it internally changed values to 0.0 -> 0, but also 1.0 -> 0.

(set-logic QF_LRA)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status sat)
(assert (and (< 0.0 1.0)))
(check-sat)
(exit)

We tracked down the error into the constructor of the GMP rational
taking a C-style string as an argument. From their site:
" The string can be an integer like '41' or a fraction like '41/152'.
The fraction must be in canonical form (see Rational Number
Functions), or if not then mpq_canonicalize must be called. "

A fast work-around converting decimal values into fractions seems to
resolve the problem.

We tested this behaviour on Arch Linux and on Ubuntu 11.10, both with
GMP.

Kind regards,
Sebastian Junges

Roberto Bruttomesso

unread,

Apr 12, 2012, 10:04:39 AM4/12/12

to ope...@googlegroups.com

Thanks for your report

With best regards,
Roberto

> --
> You received this message because you are subscribed to the Google Groups "opensmt" group.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to opensmt+u...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/opensmt?hl=en.
>