Age | Commit message (Expand) | Author |
2014-05-27 | New --tear-down-incremental mode, useful for debugging and performance profil... | Morgan Deters |
2014-05-27 | fix timespec printing | Kshitij Bansal |
2014-05-27 | Revert "timespec printing bug" | Kshitij Bansal |
2014-05-27 | timespec printing bug | Kshitij Bansal |
2014-05-27 | Fix typo in Java destruction code; should fix some recent bug reports of cras... | Morgan Deters |
2014-05-27 | Improved type-checking for tuple and record selects. | Morgan Deters |
2014-05-26 | Fix bug 567 | Kshitij Bansal |
2014-05-26 | Fixing Tim's subtype/solving bug for arrays | Clark Barrett |
2014-05-26 | Separating an implicit inclusion of smt_engine.h from theory.h. | Tim King |
2014-05-26 | Fixing a soundness bug due to the default implmentation of Theory::ppAssert()... | Tim King |
2014-05-25 | Improve quantifier instantiation: always use original terms when matching (wa... | Andrew Reynolds |
2014-05-24 | Some cleanup, fix warnings raised by Debian packager. | Morgan Deters |
2014-05-23 | Fix bug in E-matching Real/Int terms. | Andrew Reynolds |
2014-05-21 | Safer swig-wrapping for unsigned long long in Java, which will throw an excep... | Morgan Deters |
2014-05-20 | Fix compiler warning (missing virtual dtor) | Morgan Deters |
2014-05-18 | minor fix for string equality engine assertion. | Tianyi Liang |
2014-05-16 | sets: fix a bug in model building, another in handling set of sets | Kshitij Bansal |
2014-05-16 | minor improvements (fixes) to did-you-mean suggestions | Kshitij Bansal |
2014-05-15 | Minor fixes. Add SMTCOMP 2014 script. | Andrew Reynolds |
2014-05-14 | Finish --dump-instantiations option. Update scripts. | Andrew Reynolds |
2014-05-13 | Reject native extended ASCII characters. It requires user to use escaped sequ... | Tianyi Liang |
2014-05-13 | Reject un-escaped extended ASCII characters | Tianyi Liang |
2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ... | ajreynol |
2014-05-12 | Fix a bug in the IndexOf function. | Tianyi Liang |
2014-05-12 | Minor updates/fix to --cbqi-recurse | Andrew Reynolds |
2014-05-12 | Merging in additional glpk options and statistics from CAV submission. | Tim King |
2014-05-11 | Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function. | Tianyi Liang |
2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m... | Andrew Reynolds |
2014-05-09 | Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC... | Andrew Reynolds |
2014-05-08 | Major simplifications to macros module. | ajreynol |
2014-05-08 | Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min... | Andrew Reynolds |
2014-05-08 | Basic optimizations for ambqi : only normalize UF applied to variables, direc... | Andrew Reynolds |
2014-05-07 | patch to the last commit: add a single character case | Tianyi Liang |
2014-05-07 | fix a bug in contain | Tianyi Liang |
2014-05-07 | add splits | Tianyi Liang |
2014-05-07 | Fixes to ambqi, now solution-sound. | Andrew Reynolds |
2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
2014-05-05 | fix a bug in replace and contains | Tianyi Liang |
2014-05-05 | add constant regular expression check for intersection. | Tianyi Liang |
2014-05-05 | Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and c... | Morgan Deters |
2014-05-02 | Simplification of EqualityEngine::areDisequal. Comparison for production : h... | Andrew Reynolds |
2014-05-02 | Fix assertion from previous commit. | ajreynol |
2014-05-02 | Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat... | Andrew Reynolds |
2014-05-02 | More minor optimizations for datatypes. | ajreynol |
2014-05-01 | Minor optimizations to datatypes, revert to checkClash not mod eq. Minor cle... | ajreynol |
2014-05-01 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal |
2014-04-30 | decision engine: cache start index for and/or nodes | Kshitij Bansal |
2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
2014-04-29 | Fix warnings, cleanup in strings typechecker. | Morgan Deters |