Age | Commit message (Collapse) | Author |
|
|
|
Fix for emptyset in smt2 parser, sets translator to quantified logic, misc
|
|
Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.
|
|
catches some corner cases, more readable too
|
|
Fixed, at the cost of an antlr warning that's safe to ignore for now.
|
|
|
|
|
|
|
|
Sets translator, bug fixes
|
|
types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
|
|
|
|
|
|
|
|
- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine
|
|
|
|
|
|
(related to bug #569).
|
|
|
|
bvor, and bvxor.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
profiling.
|
|
sorry prvs fix added some unrelated code
|
|
This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.
|
|
|
|
crashes in Java.
|
|
|
|
This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083.
The backing Node didn't always exist because of the changes.
|
|
|
|
|
|
Theory::ppAssert() not respecting subtyping.
|
|
(was missing for simple triggers). Minor updates to scripts.
|
|
|
|
|
|
exception if the argument is out of bounds for unsigned long long. Thanks to Steve Siegel for the report.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
sequence for an extended ASCII character.
|
|
|
|
Add regressions.
|