search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
335 stars 62 forks source link

strange warning for get-value while unsat #120

Closed Ketchynez closed 4 years ago

Ketchynez commented 4 years ago

When using smt2 files as input into binary, and trying to get-value for unsat consraint, you get a strange warning expected '(' at 'a'. Maybe it would be nice to say that you just can't get values for usatisfiable constraints :)

(get-value (
  a
  b
  ...
  ))
aniemetz commented 4 years ago

You would not get this error message from calling it on unsat constraints. This is a parse error, and from the error message there should be a parenthesis missing. Hard to tell without the original input though, can you paste it?

aniemetz commented 4 years ago

Closed due to inactivity.