does not accept (model (define-fun X () Real 2) )

[jwaldmann]

opensmt uses decimal literals for real values, as in

echo "(set-logic QF_LRA)(set-option :produce-models true)(declare-fun X () Real)(assert (< 1 X)) (check-sat) (get-model)" | opensmt -p
sat
(model
(define-fun X () Real 2)
)

it seems that the smtlib2 model parser insists on 2.0, as produced by

echo "(set-logic QF_LRA)(set-option :produce-models true)(declare-fun X () Real)(assert (< 1 X)) (check-sat) (get-model)" | cvc4 --lang smt

sat

(model
(define-fun X () Real 2.0)
)

[jwaldmann]

The actual error message is

pure-matchbox: smtlib2: Unknown get-model response: 2 has type int, but real was expected.
CallStack (from HasCallStack):
  error, called at ./Language/SMTLib2/Pipe/Internals.hs:238:19 in smtlib2-pipe-1.0-K1MUvLCfPFO2upHs8kKb7q:Language.SMTLib2.Pipe.Internals

this is in getModel (not in modelEvaluate)