cvc5.git
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
2012-06-12 Dejan Jovanovićwrong answer benchmarks
2012-06-12 Dejan Jovanovićwrong result benchmark
2012-06-12 Dejan Jovanovićtests for the
2012-06-12 Dejan Jovanovićtest cases for the
2012-06-12 Clark BarrettAdding constant propagation code - needs more testing...
2012-06-12 Tim KingAdding incorrect qf_lia result.
2012-06-12 Morgan Detersfix ordering issue of --dump-to and --default-dag-thres...
2012-06-11 Tim KingFix to term normalization of integer equalities. Adds...
2012-06-11 Tim KingFixing type comparision assertion in getEqualityStatus().
2012-06-11 Dejan Jovanovićanother benchmark that used to fail
2012-06-11 Dejan Jovanovićfixing bitvector bugs
2012-06-11 Morgan Detersmark a quantifiers global var as "static" so we can...
2012-06-11 Clark BarrettOK, now the rewrite issues are fixed
2012-06-11 Morgan Detersdistribute an .expect file. fixes a "make check" failu...
2012-06-11 Morgan DetersMerge from quantifiers2-trunkmerge branch.
2012-06-11 Clark BarrettFix for array bug with decision heuristic
2012-06-11 Morgan Detersfix issue referred to in bug 352 regarding infinite...
2012-06-11 Dejan Jovanovićfailing bv examples
2012-06-11 Clark BarrettFixed bug 352
2012-06-11 Dejan Jovanovićsome failing examples
2012-06-10 Clark BarrettFixed one more bug in rewriter
2012-06-10 Clark BarrettAdded a very fruitful assertion to the rewriter: checks...
2012-06-10 Dejan Jovanovićadding an assertion to trigger the problem of bug349...
2012-06-10 Dejan Jovanovićfixes for bug347
2012-06-09 Clark BarrettTurning on unconstrained simp for QF_AUFBV
2012-06-09 Morgan DetersCleanup and comments for the dag-ifier. Also some...
2012-06-09 Morgan DetersDagification of output expressions.
2012-06-08 Morgan DetersThe option --arith-presolve-lemmas had previously been...
2012-06-08 Morgan DetersExtend Printer infrastructure also to the "Result"...
2012-06-08 Morgan Detersminor fixes, for Mac OS
2012-06-08 Dejan Jovanovićvery small fast example for the bv fail
2012-06-08 Morgan DetersFix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferri...
2012-06-08 Kshitij Bansalhandle BitVectorSignExtend in pickler
2012-06-08 Kshitij Bansalthreadlocal
2012-06-08 Kshitij BansalMerge from decision branch (till r3663)
2012-06-08 Dejan Jovanovićsmall fuzz examples where bv fails
2012-06-07 Dejan Jovanovićfixing the wrong results. arrays equality adaptor had...
2012-06-07 Morgan DetersLogicInfo locking implemented, and some initialization...
2012-06-07 Clark BarrettFixed performance issue with ite_simplifier on some...
2012-06-07 Morgan DetersAdding EchoCommand and associated printer and parser...
2012-06-07 Dejan Jovanovićcleaning up the expample for the future
2012-06-07 Clark BarrettAdded small test case for diseq propagation
2012-06-07 Dejan Jovanovićfixing some bugs in propagation of disequalities
2012-06-06 Clark BarrettDon't ever call nonclausalSimplify if simplificationMod...
2012-06-06 Clark BarrettFixed assertion failures
2012-06-06 Morgan Detersremoving std::cout from trunk
2012-06-06 Morgan Detersalso remove now-incorrect comment from makefile
2012-06-06 Clark BarrettFixed broken test case, removed one that is a mistake
2012-06-06 Morgan Detersunconstrained regressions are now run with "make check...
2012-06-06 Morgan DetersFixing numerous issues with tests and "make dist":
2012-06-06 Dejan Jovanovićdisabling a super-expensive assertions to speed up...
2012-06-06 Dejan JovanovićChanges to the combination mechanism, lots of details...
2012-06-06 Clark BarrettFixed problem causing crash at destruction time
2012-06-05 Clark BarrettMore clean-up
2012-06-05 Clark BarrettFixed a performance issue with unconstrained simplifier
2012-06-05 Clark BarrettAdding missing files...
2012-06-04 Clark BarrettAdded preprocessing pass that propagates unconstrained...
2012-06-01 Morgan Detersadd a global user-context push/pop in smt engine, just...
2012-05-31 Clark BarrettFixed bug in bv: one more case where non-shared equalit...
2012-05-31 Morgan Deterssvn:ignore a parallel-tests driver file that automake...
2012-05-31 Morgan Deterspass JAVA_CPPFLAGS properly
2012-05-30 Clark BarrettAdded BitwiseEq bitvector rewrite
2012-05-30 Clark BarrettFixed problem with array queue growing too large
2012-05-30 Morgan Detersremove unused/broken check build target
2012-05-29 Morgan Detersremoving now-unused TheoryEngine::setLogic() interface...
2012-05-29 Clark BarrettEnabled SolveEq bv rewrite
2012-05-28 Clark BarrettAdded some BV rewrites, fixed bugs in array theory...
2012-05-27 Dejan Jovanovićsome reordering to keep invariants
2012-05-27 Dejan JovanovićCommitting the work on equality engine, I need to see...
next