diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-18 00:43:53 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-18 00:43:53 -0800 |
| commit | e9bfbb2f666c8cb4cf783d8ebd398fa9304bb5b7 (patch) | |
| tree | 7280fa55e2a4c6331b71c3c0c5454b1b0b40aad6 /src/theory/bv/bitblast/bitblaster.h | |
| parent | 78d7485639cdf0769c13606b8ad3f5e9455153f1 (diff) | |
Fix ABC build (#2808)
PR #2786 introduced a pure virtual method `TBitblaster::getSatSolver()`.
`AigBitblaster` was missing the implementation of that method. This
commit adds an implementation that simply returns the underlying SAT
solver. Note: The method is currently only used for proofs and CVC4 does
not support proofs in combination with ABC. To make this explicit, the
commit also adds a check in `SmtEngine::setDefaults()` that makes sure
that we are not trying to produce proofs with `--bitblast-aig` (before
the commit, we just crashed with an assertion failure/null pointer
dereference).
Diffstat (limited to 'src/theory/bv/bitblast/bitblaster.h')
| -rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index b1fc084ed..b28ff3e2a 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -91,7 +91,7 @@ class TBitblaster bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; virtual void storeBBTerm(TNode term, const Bits& bits); - void setProofLog(proof::BitVectorProof* bvp); + virtual void setProofLog(proof::BitVectorProof* bvp); /** * Return a constant representing the value of a in the model. |