summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-07-08remove a debugging line from configure script that was left in inadvertentlyMorgan Deters
2012-07-08another signed-ness warning fix for newer GCCMorgan Deters
2012-07-08Minor changes to avoid some warnings on GCC 4.7.1 (Debian wheezy/sid). ANDY ...Morgan Deters
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-07-06Adding std namespace to a couple of make_pair instances.Tim King
2012-07-06Added include unistd to main/util.cppTim King
2012-07-06Added virtual destructor to PpRewrite.Tim King
2012-07-01Some changes to configure.ac:Morgan Deters
2012-06-28svn:ignoreMorgan Deters
2012-06-28Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2Clark Barrett
2012-06-28fix a link error on church, due to Antlr #defining "true" and "false" :-( --f...smtcomp2012-resubmissionMorgan Deters
2012-06-27Fixing a bug in proof production for the DioSolver.Tim King
2012-06-27This adds TheoryArith::safeToReset(). This fixes bug 363.Tim King
2012-06-27Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorit...Tim King
2012-06-27Improved debugging output.Tim King
2012-06-27Improved debugging output.Tim King
2012-06-27Adding reduce() to the ArithPriorityQueue. This reduces the queue from a supe...Tim King
2012-06-25Added a warning to arithmetic for a known dio solver bug. Somehow the fix nev...Tim King
2012-06-22TPTP: add parser for cnf and fofFrançois Bobot
2012-06-22parser: add some acces function and recover the original nextToken from antlr3François Bobot
2012-06-22fix : function AntlrInput::tokenTextSubstrFrançois Bobot
2012-06-22Parser: add the possibility to bind at level 0.François Bobot
2012-06-18qf_lra strategysmtcomp2012Morgan Deters
2012-06-18Reverting buggy rewriter codeClark Barrett
2012-06-18another qf_lra strategy updateMorgan Deters
2012-06-18Fixed bug in rewriterClark Barrett
2012-06-18unnecessary ^ in regular expression; warning produced on smt-execMorgan Deters
2012-06-18QF_LRA strategy in run script, now final (?) for smt-comp 2012Morgan Deters
2012-06-18final sources (?) for competitionMorgan Deters
2012-06-18Fix for slow array rewrite and minor bug fix in arrays that popped up as a re...Clark Barrett
2012-06-18small bug fix and performance fix in ite simplifierClark Barrett
2012-06-18fixed smt version 1 parser for quantifiersAndrew Reynolds
2012-06-18tracing code to make sure decision options are being set correctlyKshitij Bansal
2012-06-18bugfix, enable only QF_LRA, not other arithKshitij Bansal
2012-06-18QF_LRA, Quantifiers: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-18Fixing bug 360. The driver wasn't exiting when there was an error (it just p...Morgan Deters
2012-06-17QF_AUFLIA: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-17fixing a problem due to lemmas produced while backtrackingDejan Jovanović
2012-06-17--decision=justification-stoponly : use decision engine only for stoppingKshitij Bansal
2012-06-17enabling theoryof=term for quantifiers with sharingDejan Jovanović
2012-06-17fixing wrong assertionDejan Jovanović
2012-06-17Removed assertion that can failClark Barrett
2012-06-17fixing makefile error that brakes buildDejan Jovanović
2012-06-17Fix array bug causing incorrect answersClark Barrett
2012-06-16small change to equality assertions so that one doesn't get x = y and y = xDejan Jovanović
2012-06-16Adding the failing QF_AUFLIA regression mentioned in last commit.Kshitij Bansal
2012-06-16This is an attempt to fix the bug in the justification heuristic. TheKshitij Bansal
2012-06-16updated build script for smt-comp submissionMorgan Deters
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback