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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adding a gnu++11 rule to travis.
|
|
|
|
|
|
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.
|
|
|