diff options
Diffstat (limited to 'src/theory/bv/proof_checker.cpp')
| -rw-r--r-- | src/theory/bv/proof_checker.cpp | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp index 93ba9e67f..711e9798c 100644 --- a/src/theory/bv/proof_checker.cpp +++ b/src/theory/bv/proof_checker.cpp @@ -72,12 +72,10 @@ Node BVProofRuleChecker::checkInternal(PfRule id, { if (id == PfRule::BV_BITBLAST) { - BBSimple bb(nullptr); Assert(children.empty()); Assert(args.size() == 1); - bb.bbAtom(args[0]); - Node n = bb.getStoredBBAtom(args[0]); - return args[0].eqNode(n); + Assert(args[0].getKind() == kind::EQUAL); + return args[0]; } else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR || id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT |