Models produced by golem seem to contain elements such as -1, which are not compliant with smt-lib. When trying to validate a model with SMT solvers strictly following smt-lib, e.g., cvc5 and veriT, I get parsing errors. Solvers that are not so strict, e.g., z3 and opensmt, do not give any errors.
Example
On chc-comp24-LIA-001.smt2 the model produced under golem --print-witness contains elements such as (<= -2 (* -1 |x#6| ) ), leading to errors such as the ones below.
cvc5 error: (error "Parse Error: test.smt2:4.16: Symbol '-1' not declared as a variable")
veriT error: (error "smt2_term: unresolved symbol -1 on line 4")
Models produced by golem seem to contain elements such as
-1, which are not compliant with smt-lib. When trying to validate a model with SMT solvers strictly following smt-lib, e.g., cvc5 and veriT, I get parsing errors. Solvers that are not so strict, e.g., z3 and opensmt, do not give any errors.Example
On chc-comp24-LIA-001.smt2 the model produced under
golem --print-witnesscontains elements such as(<= -2 (* -1 |x#6| ) ), leading to errors such as the ones below.cvc5 error:
(error "Parse Error: test.smt2:4.16: Symbol '-1' not declared as a variable")veriT error:(error "smt2_term: unresolved symbol -1 on line 4")This can be fixed by substituting
-1by(- 1).