search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

TermUtils: Print negative numbers in accordance with SMT-LIB #69

Closed blishko closed 3 months ago

blishko commented 3 months ago

Unfortunately, we cannot just print the number using Logic::printSym, because this method is not overridden in ArithLogic, unlike Logic::printTerm. For now, we simply work around this by calling printTerm instead of printSym when dealing with numbers.

It would be better if OpenSMT did this directly by overriding printSym in ArithLogic as well.

Fixes #68.