diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-17 14:11:37 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-17 14:11:37 -0800 |
| commit | 332357104e9ab1937049f0ea8e53042d8534f966 (patch) | |
| tree | b92d9dd2fa7d01fa342d35fa6fccfea14ceb9514 /src/proof | |
| parent | bc40c176eb1205452e824ec9d89dc9a7c76cbd67 (diff) | |
New C++ API: Add tests for term object. (#2755)
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/bitvector_proof.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 9eb39e2e2..ba3533cc3 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -68,7 +68,7 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl; - Expr def = atom.iffExpr(atom_bb); + Expr def = atom.eqExpr(atom_bb); d_bbAtoms.insert(std::make_pair(atom, def)); registerTerm(atom); |