BUG: parse error on input -1

[pfroehle-ccl]

the following example:

produces the following output:

my guess is that the -1 has to be contained in parantheses lik this (-1) by the parser, so that cvc5 can read it right

[studJBccl]

Looks like i forgot to bracket these, will add a PR very soon.

[pfroehle-ccl]

i think there also has to be a space between the - and the 1 like this: (- 1)

[studJBccl]

I cant reproduce this.

import Language.Hasmtlib

main :: IO ()
main = do
  res <- solveWith cvc5Debug $ do
    setLogic "QF_LRA"

    x <- var @RealType
    y <- var @RealType

    assert $ (x === (-1) * (-1)) &&& (y === (-1) * (-1))  

    return (x, y)

  print res

  return ()

returns:

(set-logic QF_LRA)
(declare-fun var_1 () Real)
(declare-fun var_2 () Real)
(assert (and (= var_1 (* (- 1.0) (- 1.0))) (= var_2 (* (- 1.0) (- 1.0)))))

sat

)define-fun var_2 () Real 1.0)
(Sat,Just (1.0,1.0))

(Debugger output seems broken, will fix)

Please try to hand in a reproducable case.

[pfroehle-ccl]

i reproduced the bug with a much simpler example in the following code:

import Control.Monad.State
import Language.Hasmtlib

main :: IO ()
main = do
  res <- solveWith cvc5Debug program
  print res

program :: StateT SMT IO (Expr RealType)
program = do
  setLogic "ALL"

  let n1 = constant (-1)
  n2 <- var @RealType

  assert $ n2 === n1

  return n2

produces this:

(set-logic ALL)
(declare-fun var_1 () Real)
(assert (= var_1 -1.0))

(error "Parse Error: <stdin>:1.93: Symbol '-1.0' not declared as a variable")

*** Exception: fd:3: hFlush: resource vanished ([smtlib-backends-process] while sending command "(get-model)" to the solver: Broken pipe)