Age | Commit message (Collapse) | Author |
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
|
|
minor changes.
|
|
CASC proofs.
|
|
|
|
Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
|
|
direct handling of NOT
|
|
|
|
|
|
|
|
|
|
sets).
|
|
|
|
|
|
contract is the same as for TheoryEngine version.
|
|
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5. Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
|
|
|
|
skolemization.
|
|
|
|
clean up.
|
|
|
|
This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.
This was triggerred by a benchmark sent by andy/viktor.
performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
|