diff options
| author | lianah <lianahady@gmail.com> | 2013-02-26 16:02:52 -0500 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-02-26 16:02:52 -0500 |
| commit | f23ce9e0b40db55a62f8c830f0f4a1c9bd573dad (patch) | |
| tree | a306059ae8bc1a4bfe8cef22a5a9bfde4dcbf9f7 /src/theory/bv | |
| parent | c71ec272d5ef58bfa147507bdbb370f2e288d154 (diff) | |
| parent | c542c62d8f7c6dde84406c7e1640c029fe6cab29 (diff) | |
Merge branch '1.0.x'
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index de5b70557..57a77c0d2 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -148,7 +148,10 @@ void TheoryBV::propagate(Effort e) { bool ok = true; for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - ok = d_out->propagate(literal); + // temporary fix for incremental bit-blasting + if (d_valuation.isSatLiteral(literal)) { + ok = d_out->propagate(literal); + } } if (!ok) { |