SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

(get-value (0.0)) gives ((0.0 0)) , missing decimal point #406

Open jwaldmann opened 2 years ago

jwaldmann commented 2 years ago

this is confusing our parser (see https://github.com/yav/simple-smt/issues/20)

$ echo "(set-logic QF_LRA)(check-sat)(get-value (0.0))" | yices-smt2 --smt2-model-format
sat
((0.0 0))

other solvers output the decimal point:

$ echo "(set-logic QF_LRA)(check-sat)(get-value (0.0))" | cvc5 --produce-models
sat
((0.0 0.0))

I am using yices from recent Fedora

$ yices-smt2 --version
Yices 2.6.4
Copyright SRI International.
Linked with GMP 6.2.1
Copyright Free Software Foundation, Inc.
Build date: 2022-01-27
Platform: x86_64-pc-linux-gnu (debug)
Revision: unknown