cvc5.git
2012-06-18 Morgan DetersQF_LRA strategy in run script, now final (?) for smt...
2012-06-18 Morgan Detersfinal sources (?) for competition
2012-06-18 Clark BarrettFix for slow array rewrite and minor bug fix in arrays...
2012-06-18 Clark Barrettsmall bug fix and performance fix in ite simplifier
2012-06-18 Andrew Reynoldsfixed smt version 1 parser for quantifiers
2012-06-18 Kshitij Bansaltracing code to make sure decision options are being...
2012-06-18 Kshitij Bansalbugfix, enable only QF_LRA, not other arith
2012-06-18 Kshitij BansalQF_LRA, Quantifiers: enable use decision for (only...
2012-06-18 Morgan DetersFixing bug 360. The driver wasn't exiting when there...
2012-06-17 Kshitij BansalQF_AUFLIA: enable use decision for (only for) stopping...
2012-06-17 Dejan Jovanovićfixing a problem due to lemmas produced while backtracking
2012-06-17 Kshitij Bansal--decision=justification-stoponly : use decision engine...
2012-06-17 Dejan Jovanovićenabling theoryof=term for quantifiers with sharing
2012-06-17 Dejan Jovanovićfixing wrong assertion
2012-06-17 Clark BarrettRemoved assertion that can fail
2012-06-17 Dejan Jovanovićfixing makefile error that brakes build
2012-06-17 Clark BarrettFix array bug causing incorrect answers
2012-06-16 Dejan Jovanovićsmall change to equality assertions so that one doesn...
2012-06-16 Kshitij BansalAdding the failing QF_AUFLIA regression mentioned in...
2012-06-16 Kshitij BansalThis is an attempt to fix the bug in the justification...
2012-06-16 Morgan Detersupdated build script for smt-comp submission
2012-06-16 Dejan Jovanovićchanging theoryOf in shared mode with arrays to move...
2012-06-16 Tim KingFixing if condition for trivial equalities in arithmeti...
2012-06-15 Kshitij BansalBug fix in justification heuristic. Had to do with how
2012-06-15 Clark BarrettReverting rewrite rule to working version
2012-06-15 Clark BarrettFixes some assertion failures
2012-06-15 Clark BarrettFix for incompleteness bug with decision engine: repeat...
2012-06-15 Tim KingFixing mac compilation issues.
2012-06-15 Kshitij Bansalone bug fixed
2012-06-14 Kshitij BansalWIP
2012-06-14 Dejan Jovanovićfixing the problems with the bvminisat. there was a...
2012-06-14 Kshitij Bansaladd failing regression, move error up
2012-06-14 Tim KingFixing a case for explanation of non-normal form equali...
2012-06-14 Kshitij Bansalbug fixes in justification heuristic
2012-06-14 Tim KingFixing a bug related to explaining propagations with...
2012-06-14 Dejan Jovanovićenabling fixed bug345 case
2012-06-14 Dejan Jovanovićfixes for the hasTerm issues in the shared database...
2012-06-14 Clark BarrettNew substitutions implementation - fixes performance...
2012-06-14 Tim KingFixed arithmetic consistency issue. The simplex confli...
2012-06-14 Dejan Jovanovićfix for clark's bug
2012-06-14 Morgan Detersdon't run rewriterules regressions by default; fixes...
2012-06-14 Kshitij Bansalfix quantifier non-bug
2012-06-14 Clark BarrettRemoved an assertion, unneeded header file
2012-06-14 Morgan Deterssome changes to make CVC4 work nicely with trace execut...
2012-06-14 Morgan Detersmaking --simplification=none the default for quantified...
2012-06-14 Kshitij Bansalbug ifx, mv
2012-06-14 Kshitij Bansalrestore destruction of stuff in driver
2012-06-14 Kshitij BansalThis commit:
2012-06-14 Kshitij Bansalfailing quantifier
2012-06-14 Morgan DetersThe "no-tears-in-competition-mode" commit. Change...
2012-06-14 Kshitij Bansalfix cout, fix statname, rm deadcode
2012-06-14 Kshitij Bansaladd passing regression
2012-06-14 Dejan Jovanovićchanging to a more natural propagation order in uf...
2012-06-14 Dejan Jovanovićsome changes to the uf engine
2012-06-14 Tim KingBrings the tuning branch into trunk. This includes...
2012-06-14 Morgan Detersbug 346 resolved
2012-06-14 Dejan Jovanović* removing rewriteEquality from the rewriter
2012-06-13 Dejan Jovanovićremoving bug233 until morgan commits the actual file
2012-06-13 Morgan Detersadding some regressions to the usual regressions runs...
2012-06-13 Tim KingAdded witnesses to Constraints.
2012-06-13 Tim King- Added a loop to internally assert constraints that...
2012-06-13 Tim KingFixed whitespace warning on Makefile.
2012-06-13 Tim KingAdds debugging output to theory_engine.cpp.
2012-06-13 Morgan Detersrevisions to the "make submission" target
2012-06-13 Morgan DetersDon't use the "inlined" feature of ANTLR 3.2, which...
2012-06-13 Kshitij Bansaladd passing regression
2012-06-13 Dejan Jovanovićfix for bug 354
2012-06-13 Clark BarrettFixed failing assertion when EqualityEngine is in conflict
2012-06-13 Dejan Jovanovićenabling regressions from last night, all fixed
2012-06-13 Kshitij Bansalenable some decision regressions
2012-06-13 Kshitij BansalMake d_result in DE context dependent
2012-06-13 Clark BarrettFixed definition of bvsmod
2012-06-13 Kshitij Bansaldecision regressions, all but one fail
2012-06-13 Clark BarrettFixes more problems in bv rewrites
2012-06-13 Dejan Jovanović!(*child_it).isConst() assertion fail
2012-06-13 Dejan Jovanovićr2.node == response.node failure
2012-06-13 Dejan Jovanovićr2.node == response.node failure
2012-06-13 Dejan Jovanović!current[0].isConst() failure
2012-06-13 Clark BarrettFixes lots of problems in bv rewrite rules and adds...
2012-06-13 Dejan Jovanovićbenchmark to show that we don't rewrite bvsmod correctly
2012-06-12 Morgan DetersFix some compile warnings (but they never showed up...
2012-06-12 Morgan DetersFix to SMT-LIBv1 parser: QF_UF declares sort "U", but...
2012-06-12 Dejan Jovanovićmissing problems
2012-06-12 Dejan Jovanovićwrong answer for bv
2012-06-12 Clark BarrettMoved some things around in the preprocessor. Now...
2012-06-12 Clark BarrettFixed fuzzing bug
2012-06-12 Tim KingFix to yesterday's change in arithmetic.
2012-06-12 Kshitij Bansalbv reduced with decision: sat instead of unsat
2012-06-12 Kshitij BansalAssert fail equaility_engine.cpp: hasTerm(node) with...
2012-06-12 Dejan Jovanovićbufixes and the bugs
2012-06-12 Dejan Jovanovićconflicts from theories are removable
2012-06-12 Clark BarrettChanged bitvector theory rewriter so that equalities...
2012-06-12 Kshitij Bansalcleanup of exit mechanism when decisionEngine is on...
2012-06-12 Clark BarrettFixed bug causing QF_LIA/solver_cvc4/incorrect1.smt...
2012-06-12 Clark BarrettFixed failing assertion in arrays for bug 347
2012-06-12 Dejan Jovanovićmore breakage in aufbv
2012-06-12 Morgan Detersminor cleanup, and replace a "private:" in equality...
2012-06-12 Clark BarrettFixed compile error
2012-06-12 Clark BarrettEnabling constant propagation
2012-06-12 Morgan Detersfix a few compatibility bindings issues
next