Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
Brain for reporting this.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
segfault in smt2 printer
|
|
|
|
|
|
|
|
were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
|
|
|
|
|
|
|
|
|
|
|
|
Deligiannis.
|
|
|
|
|
|
|
|
to be simplified by check-model in that case.
|
|
|
|
|
|
|
|
|
|
|
|
suggestions
|
|
|
|
|
|
infrastructure to BV collectModelInfo in preparation for bug fix.
|
|
|
|
|
|
engine.
|
|
|
|
|
|
|
|
--no-condense-function-values
|
|
|
|
|
|
|
|
|
|
|
|
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
|