Age | Commit message (Expand) | Author |
2012-10-09 | fixed bv rewriter to evaluate bvurem over constants | Liana Hadarean |
2012-10-09 | More fixes to model code | Clark Barrett |
2012-10-09 | made datatypes rewrite incorrect selectors to ground term. this feature can ... | Andrew Reynolds |
2012-10-09 | usability: remove --no-interactive from --smtlib option | Morgan Deters |
2012-10-09 | fix for bug 415 | Dejan Jovanović |
2012-10-09 | * Add assertion in TheoryModel code to ensure we don't get inconsistent | Morgan Deters |
2012-10-09 | fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4... | Morgan Deters |
2012-10-09 | some documentation fixes | Morgan Deters |
2012-10-09 | adding mergePredicates method to the equality engine to be able to | Dejan Jovanović |
2012-10-08 | * Models' SubstitutionMaps are now attached to the user context | Morgan Deters |
2012-10-08 | added reduced bv model failing test case | Liana Hadarean |
2012-10-08 | Fixed problem in assertEqualityEngine: predicates that are not false are no | Clark Barrett |
2012-10-08 | small fix for compat JNI library installation | Morgan Deters |
2012-10-08 | fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't a... | Morgan Deters |
2012-10-06 | turn off cudd by default in configure script | Morgan Deters |
2012-10-06 | * more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASS | Morgan Deters |
2012-10-06 | * Clean up some options documentation | Morgan Deters |
2012-10-06 | * Some documentation about building compatibility and language bindings | Morgan Deters |
2012-10-06 | * Include a few bug testcases for resolved bugs. | Morgan Deters |
2012-10-06 | * Fix some regressions' expected outputs. | Morgan Deters |
2012-10-05 | fix \file | Morgan Deters |
2012-10-05 | Bug-related: | Morgan Deters |
2012-10-05 | BoolExpr removed and replaced with Expr | Dejan Jovanović |
2012-10-04 | disable model-generation by default in cvc3 compatibility layer. should fix ... | Morgan Deters |
2012-10-04 | Implemented array type enumerator, more fixes for models | Clark Barrett |
2012-10-04 | IllegalArgumentException in java needs to be named "CVC4IllegalArgumentExcept... | Morgan Deters |
2012-10-03 | minor fix for mbqi in finite model finding | Andrew Reynolds |
2012-10-03 | implemented collectModelInfo for TheoryBV | Liana Hadarean |
2012-10-03 | updates to contrib scripts to match docs | Morgan Deters |
2012-10-03 | better documentation, allow examples to be installed, etc | Morgan Deters |
2012-10-03 | New model code, mostly workin | Clark Barrett |
2012-10-03 | new README and INSTALL files | Morgan Deters |
2012-10-03 | added support for interrupting TheoryBV | Liana Hadarean |
2012-10-03 | --wait-to-join / --no-wait-to-join option | Kshitij Bansal |
2012-10-03 | adding ::getBooleanVariables to the PropEngine | Dejan Jovanović |
2012-10-02 | * re-enable some Z3 extended commands: | Morgan Deters |
2012-10-02 | workaround for a nasty CLN bug | Morgan Deters |
2012-10-01 | "Fix" (disable) portfolio when using quantifiers | Kshitij Bansal |
2012-10-01 | make sure to mark LogicInfo as CVC4_PUBLIC | Morgan Deters |
2012-10-01 | fix for dejan: term ITEs now dumped correctly | Morgan Deters |
2012-10-01 | initial draft of skolemization during pre-processing, made simple cliques the... | Andrew Reynolds |
2012-09-30 | minor changes to arithmetic assertions involving nonlinearity and models (rel... | Morgan Deters |
2012-09-30 | minor fixes to pickler (hopefully fixes Debian build from last night) | Morgan Deters |
2012-09-30 | release notes | Morgan Deters |
2012-09-29 | Calling the setIncompleteness() flag on all full checks once a non-linear ter... | Tim King |
2012-09-29 | Fix a few segfaults in driver. | Morgan Deters |
2012-09-29 | draft RELEASE-NOTES file, and minor release stuff | Morgan Deters |
2012-09-29 | fixes to "make distclean" and C compatibility bindings; should fix the broken... | Morgan Deters |
2012-09-29 | fixes to "make distclean" and C compatibility bindings; should fix the broken... | Morgan Deters |
2012-09-29 | This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ... | Tim King |