summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-06-08very small fast example for the bv failDejan Jovanović
2012-06-08Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).Morgan Deters
2012-06-08handle BitVectorSignExtend in picklerKshitij Bansal
2012-06-08threadlocalKshitij Bansal
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-06-08small fuzz examples where bv fails Dejan Jovanović
2012-06-07fixing the wrong results. arrays equality adaptor had a missing case when pro...Dejan Jovanović
2012-06-07LogicInfo locking implemented, and some initialization-order issues in SmtEng...Morgan Deters
2012-06-07Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarksClark Barrett
2012-06-07Adding EchoCommand and associated printer and parser rules:Morgan Deters
2012-06-07cleaning up the expample for the futureDejan Jovanović
2012-06-07Added small test case for diseq propagationClark Barrett
2012-06-07fixing some bugs in propagation of disequalitiesDejan Jovanović
2012-06-06Don't ever call nonclausalSimplify if simplificationMode = NONE (even ifClark Barrett
2012-06-06Fixed assertion failuresClark Barrett
2012-06-06removing std::cout from trunkMorgan Deters
2012-06-06also remove now-incorrect comment from makefileMorgan Deters
2012-06-06Fixed broken test case, removed one that is a mistakeClark Barrett
2012-06-06unconstrained regressions are now run with "make check", but with --unconstra...Morgan Deters
2012-06-06Fixing numerous issues with tests and "make dist":Morgan Deters
2012-06-06disabling a super-expensive assertions to speed up debug runsDejan Jovanović
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-06-06Fixed problem causing crash at destruction timeClark Barrett
2012-06-05More clean-upClark Barrett
2012-06-05Fixed a performance issue with unconstrained simplifierClark Barrett
2012-06-05Adding missing files...Clark Barrett
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-06-01add a global user-context push/pop in smt engine, just like clark's addition ...Morgan Deters
2012-05-31Fixed bug in bv: one more case where non-shared equality was getting propagatedClark Barrett
2012-05-31svn:ignore a parallel-tests driver file that automake deposits in config/Morgan Deters
2012-05-31pass JAVA_CPPFLAGS properlyMorgan Deters
2012-05-30Added BitwiseEq bitvector rewriteClark Barrett
2012-05-30Fixed problem with array queue growing too largeClark Barrett
2012-05-30remove unused/broken check build targetMorgan Deters
2012-05-29removing now-unused TheoryEngine::setLogic() interface functionMorgan Deters
2012-05-29Enabled SolveEq bv rewriteClark Barrett
2012-05-28Added some BV rewrites, fixed bugs in array theory, made ite simp work with BVClark Barrett
2012-05-27some reordering to keep invariantsDejan Jovanović
2012-05-27Committing the work on equality engine, I need to see how it does on the regr...Dejan Jovanović
2012-05-27Another expensive function call in a Debug traceClark Barrett
2012-05-27Another expensive function call in a Debug lineClark Barrett
2012-05-25init bug fixKshitij Bansal
2012-05-25Checking in fix for bug 340 - somehow didn't get checked in earlierClark Barrett
2012-05-24Separating the subtheory implementations in the bitvector theory.Dejan Jovanović
2012-05-24Significant changes to the internals of the equality engine. Equality is not ...Dejan Jovanović
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-21Updating equality manager to handle tagged trigger terms. Notifications are p...Dejan Jovanović
2012-05-21main() no longer catches non-CVC4 exceptions. This means on memout and other...Morgan Deters
2012-05-19Adding regress test for bug 341.Tim King
2012-05-19- The array type rules were fixed to use isSubtypeOf.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback