cvc4/cvc4-boolean.patch
Jerry James ebc8ce8c1a Add -boolean, -minisat, and -signed patches to fix test failures.
Also:
- Fix boost detection with g++ 5.0.
- Fix access to an uninitialized variable.
- Help the documentation generator find COPYING.
- Build with -fsigned-char to fix the arm build.
- Prevent rebuilds while running %check.
2015-03-11 22:26:03 -06:00

23 lines
1.3 KiB
Diff

--- ./src/theory/bv/bv_subtheory_algebraic.cpp.orig 2014-07-13 11:32:35.951598886 -0600
+++ ./src/theory/bv/bv_subtheory_algebraic.cpp 2015-03-08 20:00:000000000000 -0600
@@ -465,7 +465,7 @@ bool AlgebraicSolver::solve(TNode fact,
if (right.getKind() == kind::BITVECTOR_XOR &&
left.getKind() == kind::BITVECTOR_XOR) {
TNode var = left[0];
- if (!var.getMetaKind() == kind::metakind::VARIABLE)
+ if (var.getMetaKind() != kind::metakind::VARIABLE)
return false;
// simplify xor with same variable on both sides
--- ./src/theory/bv/bv_subtheory_core.cpp.orig 2014-07-13 11:32:35.959599119 -0600
+++ ./src/theory/bv/bv_subtheory_core.cpp 2015-03-08 20:00:00.000000000 -0600
@@ -291,7 +291,7 @@ void CoreSolver::buildModel() {
bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
// Notify the equality engine
- if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+ if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_CORE)) {
Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
// Debug("bv-slicer-eq") << " reason=" << reason << endl;
bool negated = fact.getKind() == kind::NOT;