summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-07-27Minor cleanup after today's commits:Morgan Deters
2012-07-27removing unecessary filesAndrew Reynolds
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to mod...Andrew Reynolds
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-26Datatype enumerator work. This version is not a "fair" enumerator, but I got...Morgan Deters
2012-07-18more compliance fixes for SMT-LIBv2Morgan Deters
2012-07-18a few fixes for java system testMorgan Deters
2012-07-18small change to model-generation function, after discussion w/ AndyMorgan Deters
2012-07-18removing an obsolete assertion in model-generation framework, per Andy's requestMorgan Deters
2012-07-18removing output operator for SExprTypes, which is never used (and SExprTypes ...Morgan Deters
2012-07-17SMT-LIBv2 compliance updates:Morgan Deters
2012-07-17minor fix to prevent getValue from returning nullAndrew Reynolds
2012-07-17fix for --produce-models with CVC4 presentation languageMorgan Deters
2012-07-17fix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---bu...Morgan Deters
2012-07-16now passes "make distcheck", which does important checks for the release (e.g...Morgan Deters
2012-07-16fix compiler warning in unit testMorgan Deters
2012-07-16stronger two_smt_engines testMorgan Deters
2012-07-16fix inadvertent change to system testMorgan Deters
2012-07-16Support for having two SmtEngines with the same ExprManager.Morgan Deters
2012-07-16found a bug in the initialization order of UF, EqualityEngine, and the UF str...Morgan Deters
2012-07-16reverse the order of link arguments to -lcln -lgmp, fixes linking errors for ...Morgan Deters
2012-07-14Type enumerator infrastructure and uninterpreted constant support. No suppor...Morgan Deters
2012-07-14Applying Dejan's patch for bug #369, which resolves it by adding a new (let.....Morgan Deters
2012-07-14fixing make distMorgan Deters
2012-07-14fix a warning in unit test compilationMorgan Deters
2012-07-14svn ignoreMorgan Deters
2012-07-14an example that uses bitvectors to simulate sha1 computation and dumps an smt...Dejan Jovanović
2012-07-12removing readme from fmf-develAndrew Reynolds
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-10svn ingoreMorgan Deters
2012-07-10* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)Dejan Jovanović
2012-07-10going back to 1. being a non decimalDejan Jovanović
2012-07-10small changes:Dejan Jovanović
2012-07-09minor fix-upsMorgan Deters
2012-07-09fix portfolio buildMorgan Deters
2012-07-09fix eXecutable bit on a scriptMorgan Deters
2012-07-08minor SMT-LIBv2 compliance issuesMorgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback