summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Collapse)Author
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-26Removing DioSolver::acceptableOriginalNodes(). This assertion was too ↵Tim King
strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
2012-11-26Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run ↵Tim King
in debug mode. This is too long for a regress0 test.
2012-11-25Adding a regression test from bug 462.Tim King
2012-11-23Example of rewrite rules use that comes from an harness testFrançois Bobot
2012-11-19Adding hand minimized test for bug 450.Tim King
2012-11-17Fixed last currently known bug in array modelsClark Barrett
2012-11-17* enable previously-failing (now succeeding) datatype example that uses recordsMorgan Deters
* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-16Fix for bug451Clark Barrett
2012-11-15More fixes to model generation, with previously failing testcasesClark Barrett
Also refactored some header file includes to reduce compile time
2012-11-15fuzz15 should have been fuzz14Clark Barrett
2012-11-15Fixed another AUFBV model bug. BV equality subtheory needed to do somethingClark Barrett
similar to arrays - limit the set of terms reported to those relevant in the current context. Also removed collectModelInfo from sharedTermsDatabase - doesn't seem to be needed any more.
2012-11-15Fixing comments in print_lambda.cvc.Tim King
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ↵Tim King
printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
2012-11-14Fix to bug449. Adds shared constants to the set of DeltaRationals that must ↵Tim King
be in the final total order.
2012-11-14bug fixes to models, array rewriter with previously failing testcasesClark Barrett
2012-11-13added support for division by zero for bit-vector division operatorsLiana Hadarean
2012-11-13Fixed an array rewriting bug found by fuzzerClark Barrett
2012-11-13Testcases for fixed bugsClark Barrett
2012-11-12Improved error reporting for improperly using non-linear division in linear ↵Tim King
arithmetic.
2012-11-12Delta is now generated in arithmetic to keep consistent the total order of ↵Tim King
DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
2012-11-10Fixed missing \ in uflra/Makefile.maClark Barrett
Fixed another model bug and added previously failing fuzz testcase
2012-11-10Fix for bug 439. Delta computation now includes disequality information.Tim King
2012-11-09Test that breaks arithmetic model building due to disequality terms.Tim King
2012-11-09Arithmetic problem that fails --check-models due incompleteness with ↵Tim King
multiplication.
2012-11-08Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases ↵Tim King
for division by 0.
2012-11-07* Type ascription bug fixed (resolves bug 432), but there are others I ↵Morgan Deters
discovered (still outstanding). :-( * Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night) * Provide expected output for arith regression 'mod.01.smt2' * Also, fix a compiler warning in inst_gen.cpp (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-07Fix to a bug in integer mod lemmas.Tim King
2012-10-30delta of a model-building failure caseDejan Jovanović
2012-10-26fixed bug in datatypes decision procedure enforcing rewriting of incorrectly ↵Andrew Reynolds
applied selector terms, this effects two regression test where TCC fails, using --disable-dt-rewrite-error-sel changes answer of both regression tests
2012-10-24fix for bug 429 Dejan Jovanović
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
2012-10-24two smaller random pure LRA push-pop cases that failDejan Jovanović
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_01.smt2 z3: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat sat cvc4: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat unsat dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_02.smt2 z3: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat sat cvc4: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat unsat
2012-10-23fixed problem with datatypes giving incorrect explanations, now corrected ↵Andrew Reynolds
and improved. this update fixes bug 428, also changes the result for 2 benchmarks where tcc in cvc3 fails (cvc4 had previously had been answering correctly by accident).
2012-10-22add bug 425 models regression; fix mac-build execute permissionMorgan Deters
2012-10-11Fix bug 421, again, and add a second, independent test case for the sameMorgan Deters
with --check-models (which caused the same bug, for a different reason, due to some unintended interaction between the checkModel() function and the UserContext, which rolled back the Model object. (Groan...) (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-10Abstract values for SMT-LIB.Morgan Deters
Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
* fix minor issue with s-expr parsing in CVC and SMT grammars * other minor things (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09made datatypes rewrite incorrect selectors to ground term. this feature can ↵Andrew Reynolds
be turned off by --disable-dt-rewrite-error-sel. changed regression answer to reflect new default behavior.
2012-10-09fix beta reduction in both preRewrite() *and* postRewrite(), related to bug ↵Morgan Deters
417. oops. also fix spelling on "rewritting" test
2012-10-08added reduced bv model failing test caseLiana Hadarean
2012-10-06* Include a few bug testcases for resolved bugs.Morgan Deters
* Fix error message if you POP beyond the bottom user stack frame. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
* Ensure Rewriter::init() is called before ::rewrite(). The array type enumerator recently gave us an end-run around ::init(). TheoryEngine no longer calls these, they're done via static initialization. * Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-09-26bug #398 test (bug was resolved last night), and a script to download all ↵Morgan Deters
bug attachments from bugzilla and put them in the tree
2012-09-25some buggy examples for incrementality, and make bug326 run as part of make ↵Morgan Deters
regress, because the bug was fixed. Also make QuantifiersModule's destructor virtual (it has virtual members). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-24some api changesDejan Jovanović
2012-09-21Fixes for datatype dumping and printing. Add a new test case for dumping.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and TheoryBuiltin rewriter support (resolves bug #383) * with --smtlib2, force interactive mode off by default Also: * fix a few bugs causing crashes * better "alias" processing for options * configure-time fixes to readline detection (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-18SMT-LIBv2 compliance regarding outputting "unknown".Morgan Deters
Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback