Age | Commit message (Collapse) | Author |
|
|
|
A bug was introduced in the cleanup process as preparation for the merge
(theory_sets_private.cpp, lines 2502-2508 in this commit).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
strictly earlier entries.
|
|
|
|
|
|
|
|
|
|
we can deduce that it is a constant-disequality proof and process it accordingly
|
|
|
|
|
|
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
|
|
|
|
|
|
default in EPR mode.
|
|
|
|
|
|
|
|
to EPR
|
|
|
|
|
|
|
|
|
|
breaking in theory sep.
|
|
|
|
allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
|
|
|
|
miniscoping in prenex normal form.
|
|
|
|
Relaxing the throw specifiers for the destructors for Node, TypeNode,…
|
|
changes for cbqi.
|
|
|
|
quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
|
|
context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.
|
|
|
|
|
|
|
|
|
|
|
|
|