yices2 icon indicating copy to clipboard operation
yices2 copied to clipboard

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

Open jwaldmann opened this issue 3 years ago • 0 comments

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

jwaldmann avatar Aug 17 '22 17:08 jwaldmann