Age | Commit message (Expand) | Author |
2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use assertRepre... | ajreynol |
2014-11-06 | Reenable regression. Add (for now, disabled) changes to datatypes theory com... | ajreynol |
2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not assi... | ajreynol |
2014-11-01 | Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemma... | ajreynol |
2014-11-01 | Fix some mistakes in datatypes theory combination, disable two regressions. ... | ajreynol |
2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in mod... | ajreynol |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters |
2014-10-22 | Fix bug590 regression distcheck failure from last night. | Morgan Deters |
2014-10-21 | Fixed bug 590, added regression test | Clark Barrett |
2014-10-10 | Merge remote-tracking branch 'origin/1.4.x' | Kshitij Bansal |
2014-10-10 | Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti... | Kshitij Bansal |
2014-10-06 | Merge branch '1.4.x' | Morgan Deters |
2014-10-06 | Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report. | Morgan Deters |
2014-10-06 | Merge branch '1.4.x' | Morgan Deters |
2014-10-06 | fix for bug586 | Kshitij Bansal |
2014-10-06 | Extended parsing testcase, with constant arrays and RESET. | Morgan Deters |
2014-10-06 | Merge branch '1.4.x' | Morgan Deters |
2014-10-06 | Fix native language parsing of chained-store expressions (resolves bug 585). ... | Morgan Deters |
2014-10-04 | Enable some old bug testcases that (maybe?) never got added. | Morgan Deters |
2014-10-03 | Add some (so far trivial) regressions for constant arrays. | Morgan Deters |
2014-09-24 | Fix infinite loop in datatypes enumerator. Minor work on conjecture generator. | ajreynol |
2014-09-17 | Fix soundness bug for quantifier macros involving Int/Real. | ajreynol |
2014-09-03 | Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change... | ajreynol |
2014-08-28 | fixing bug580 caused by bad bv inequality explanation | lianah |
2014-08-28 | fixing bug580 caused by bad bv inequality explanation | lianah |
2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters |
2014-08-22 | Merge branch '1.4.x' | Morgan Deters |
2014-08-22 | Fix incorrectly-labeled test. | Morgan Deters |
2014-08-18 | Merge branch '1.4.x' | Morgan Deters |
2014-08-18 | Revert a8e0ce67 and add test case (resolves bug #578). | Morgan Deters |
2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters |
2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters |
2014-07-25 | patch for regular expression intersection caching | Tianyi Liang |
2014-07-12 | Status for new bug testcase. | Morgan Deters |
2014-07-12 | Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre f... | Morgan Deters |
2014-07-10 | membership cvc token changed to `IS_IN' to avoid conflict with IN used for let | Kshitij Bansal |
2014-07-09 | sets cvc parser | Kshitij Bansal |
2014-07-09 | sets cvc printer | Kshitij Bansal |
2014-06-30 | Merge pull request #45 from mdeters/turn-off-strings-exp | Morgan Deters |
2014-06-30 | Merge pull request #47 from kbansal/sets | Kshitij Bansal |
2014-06-30 | Use FS as the set-logic string for theory of sets | Kshitij Bansal |
2014-06-29 | sets: "insert" operator | Kshitij Bansal |
2014-06-27 | Fix for bug543 | Clark Barrett |
2014-06-25 | Turn strings-exp off by default (for the release) | Morgan Deters |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are now... | Kshitij Bansal |
2014-06-23 | Fatal error if --unconstrained-simp and --produce-models used together (befor... | Morgan Deters |
2014-06-22 | Renaming of SMT2 operator names, kinds for set theory | Kshitij Bansal |
2014-06-19 | forgot to add the test with fix | Kshitij Bansal |
2014-06-19 | disable unate lemmas when using incremental mode | Kshitij Bansal |
2014-06-13 | fixed BVMinisat bug due to not clearing seen properly | lianah |