diff options
| author | lianah <lianahady@gmail.com> | 2013-02-26 15:50:37 -0500 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-02-26 15:50:37 -0500 |
| commit | dec5c322b84e45659e3683d16b42a4b6d648b172 (patch) | |
| tree | e089b6d88d9235072adfa766f0daed71b7ba8b0f /src/theory/bv/theory_bv.cpp | |
| parent | 63ca7c0a10dcd6b3be42d4d513f842db76733392 (diff) | |
fix for bv crash in incremental mode; this is a temporary fix for bug 493
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -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 7acb93cc2..8baa31a4b 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) { |