summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith
AgeCommit message (Expand)Author
2016-11-17Fix Makefiles in testAndres Notzli
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal type...Tim King
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-02-19Merge branch '1.3.x'Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-04Remove a regression for which the portfolio takes forever (see bug 542).Morgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-11Change exit status to be more consistent with other command-line tools: 0 suc...Morgan Deters
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Move some regress benchmarks around that took too long, other test cleanup.Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-04-26FCSimplex branch mergeTim King
2013-03-19Fixes for miplib-trick application (and a new testcase)Morgan Deters
2013-02-05Fix to miplib trick to make it less "cautious" and apply in more casesMorgan Deters
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-11-12Improved error reporting for improperly using non-linear division in linear a...Tim King
2012-11-12Delta is now generated in arithmetic to keep consistent the total order of De...Tim King
2012-11-09Arithmetic problem that fails --check-models due incompleteness with multipli...Tim King
2012-11-08Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases fo...Tim King
2012-11-07* Type ascription bug fixed (resolves bug 432), but there are others I discov...Morgan Deters
2012-11-07Fix to a bug in integer mod lemmas.Tim King
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions shou...Morgan Deters
2012-06-14Fixed arithmetic consistency issue. The simplex conflict variable had to be ...Tim King
2012-06-12Adding incorrect qf_lia result.Tim King
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-05-07Fixes a sign bug in the DioSolver.Tim King
2012-04-18add the missing BINARY variable in some test/regress makefilesKshitij Bansal
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ba...Morgan Deters
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
2012-02-20portfolio mergeMorgan Deters
2012-02-16Last commit accidentally lacked r2778 and r2779 from integer2. I have manual...Tim King
2012-02-07removing the 100 integer benchmarks from regress0, too manyDejan Jovanović
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-10-19Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 i...Tim King
2011-10-17Sharing workDejan Jovanović
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-05-31This commit contains the code for allowing arbitrary equalities in the theory...Tim King
2011-03-26fix typoMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2010-10-29Adds a very small test that triggers a bug. The bug is from the commit for -r...Tim King
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback