summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Expand)Author
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
2017-05-31Minor change to defaults, update smt comp script, minor changes to options in...ajreynol
2017-03-28Fix bug 787.ajreynol
2017-03-28Fix for bug 733Clark Barrett
2017-03-24Add some regressions. Minor.ajreynol
2017-01-05Disabling a regression test that assumes CVC4 is configured with proofs on. M...Tim King
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres Notzli
2016-12-02Fix for bug 734Clark Barrett
2016-11-30Remove wrong `ExtractMultLeadingBit` ruleAndres Notzli
2016-11-17Fix Makefiles in testAndres Notzli
2016-11-11Add simple inferences for extended bitvector functions, add a few related opt...ajreynol
2016-10-26Enable bv2nat regressionsajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2014-06-13fixed BVMinisat bug due to not clearing seen properlylianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes cas...Morgan Deters
2014-03-11Minor cleanup.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
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-04-26Merge experimental decisionweight branchKshitij Bansal
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-21added regression test for constant evallianah
2013-03-20added more testslianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ineq...lianah
2013-03-20one more ineq regressionLiana Hadarean
2013-03-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
2013-03-16started work on the inequality bv subtheorylianah
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-11-13Testcases for fixed bugsClark Barrett
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-08added reduced bv model failing test caseLiana Hadarean
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions shou...Morgan Deters
2012-06-28Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2Clark Barrett
2012-06-14fix for clark's bugDejan Jovanović
2012-06-13enabling regressions from last night, all fixedDejan Jovanović
2012-06-13!(*child_it).isConst() assertion failDejan Jovanović
2012-06-13r2.node == response.node failure Dejan Jovanović
2012-06-13!current[0].isConst() failureDejan Jovanović
2012-06-13benchmark to show that we don't rewrite bvsmod correctlyDejan Jovanović
2012-06-12wrong answer for bvDejan Jovanović
2012-06-12bv reduced with decision: sat instead of unsatKshitij Bansal
2012-06-12wrong answer benchmarksDejan Jovanović
2012-06-11another benchmark that used to fail Dejan Jovanović
2012-06-11fixing bitvector bugsDejan Jovanović
2012-06-11failing bv examplesDejan Jovanović
2012-06-08very small fast example for the bv failDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback