summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-14Fixing cryptominisat build issuesexperimentalLiana Hadarean
2015-10-14Added get-cryptominisat4 script.Liana Hadarean
2015-06-17minor fixes to sat solversLiana Hadarean
2015-06-15Make array basis term a skolem (avoids crashing in fmf).smtcomp2015-experimentalajreynol
2015-06-15fixes to QF_BV and QF_UFBV run scriptLiana Hadarean
2015-06-14dummy commit to mark adding crpytominisat to configure in competition binaryKshitij Bansal
2015-06-14Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-14mergeLiana Hadarean
2015-06-14changes to run script and minor bvLiana Hadarean
2015-06-15Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyPr...Tim King
2015-06-14Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-14Handing the case in replay where a cut is directly in conflict with an existi...Tim King
2015-06-14added ackermanization for eager bit-blastingLiana Hadarean
2015-06-14Merge branch 'nonlinearaxiomhack' into experimentalTim King
2015-06-14Guarding the new axiom list for arithmetic division symbols a bit stronger.Tim King
2015-06-14More updates for QF_NIAClark Barrett
2015-06-14Potential fix for non-linear axioms in incremental mode.Tim King
2015-06-14teardown for nonlinearKshitij Bansal
2015-06-14Strengthening the Assertions for QF_NIA -> QF_BV pass.Tim King
2015-06-14Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-14Fix for UMINUS translation in intToBV passClark Barrett
2015-06-14Fix for potential cache problem in intToBV passClark Barrett
2015-06-14Updated run script for QF_NIAClark Barrett
2015-06-14Updated run script for QF_NIAClark Barrett
2015-06-14Added option for converting QF_NIA to bitvectorsClark Barrett
2015-06-14Fixes for shared term normalization in replay for constraint construction.Tim King
2015-06-14Fixes for shared term normalization in replay for constraint construction.Tim King
2015-06-14Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-14Turning off aggressive arith ite simplifications during incremental solving.Tim King
2015-06-14Turning off aggressive arith ite simplifications during incremental solving.Tim King
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Robust check to avoid store all instantiations. Fix prior commit for sort inf...ajreynol
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Changing the run script for master for the application track.Tim King
2015-06-13Removing extra arguments for --incremental solving in run-script-smtcomp2015-...Tim King
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Restricting TheoryArith to computeRelevantTerms.Tim King
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Disable sort inference for experimental runscriptKshitij Bansal
2015-06-13Disable sort inference for SMT COMPajreynol
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Fixed bug in iteSimpClark Barrett
2015-06-13Fixed bug in iteSimpClark Barrett
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Fix for assertion failure:Clark Barrett
2015-06-13Fix for sort inference involving mixed Int/Real equalities.ajreynol
2015-06-13A return value for an ApproxGLPK::loadVB() failure case was incorrect.Tim King
2015-06-13A return value for an ApproxGLPK::loadVB() failure case was incorrect.Tim King
2015-06-13Merge remote-tracking branch 'origin/master' into experimentalKshitij Bansal
2015-06-13Avoid instantiating with array constants.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback