Sebastian Junges
unread,Apr 12, 2012, 4:41:50 AM4/12/12Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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