summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-01-18 00:43:53 -0800
committerGitHub <noreply@github.com>2019-01-18 00:43:53 -0800
commite9bfbb2f666c8cb4cf783d8ebd398fa9304bb5b7 (patch)
tree7280fa55e2a4c6331b71c3c0c5454b1b0b40aad6 /contrib
parent78d7485639cdf0769c13606b8ad3f5e9455153f1 (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 'contrib')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback