search

yav / simple-smt

BSD 3-Clause "New" or "Revised" License
20 stars 20 forks source link

output format of negative Reals not accepted by cvc5 #17

Open jwaldmann opened 2 years ago

jwaldmann commented 2 years ago

I have this constraint

     x <- declare s "x" tReal
     assert s (mul (real 3) (add x (real 2)) `eq` real (negate 5))

communicating with cvc5 gives

[send->] (assert (= (* 3.0 (+ x 2.0)) -5.0))
[<-recv] (error "Parse Error: <stdin>:4.33: Symbol -5.0 is not declared. (assert (= (* 3.0 (+ x 2.0)) -5.0)) ^ ")
ex3: user error (Unexpected result from the SMT solver:
  Expected: success
  Result: (error "Parse Error: <stdin>:4.33: Symbol -5.0 is not declared. (assert (= (* 3.0 (+ x 2.0)) -5.0)) ^ ")
)

I guess they want (- 5.0) instead of -5.0.