diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-08 20:16:33 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-08 20:16:33 -0800 |
| commit | 707e27e61addafdbcce5e7b6d32a61985f563dfb (patch) | |
| tree | 0ec51ee2c84c9294123b48ff7734d9cd7fcbc06c /src/theory/bv/bvgauss.cpp | |
| parent | 215c41d35390927409aac3827798f89d82f6b4bb (diff) | |
Add bv util mkConst(unsigned, Integer&). (#1499)
Diffstat (limited to 'src/theory/bv/bvgauss.cpp')
| -rw-r--r-- | src/theory/bv/bvgauss.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp index cfdab57be..d0e2266a7 100644 --- a/src/theory/bv/bvgauss.cpp +++ b/src/theory/bv/bvgauss.cpp @@ -582,8 +582,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( /* Normalize (no negative numbers, hence no subtraction) * e.g., x = 4 - 2y --> x = 4 + 9y (modulo 11) */ Integer m = iprime - lhs[prow][i]; - Node bv = - nm->mkConst<BitVector>(BitVector(utils::getSize(vvars[i]), m)); + Node bv = utils::mkConst(utils::getSize(vvars[i]), m); Node mult = nm->mkNode(kind::BITVECTOR_MULT, vvars[i], bv); stack.push_back(mult); } @@ -602,8 +601,8 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( if (rhs[prow] != 0) { tmp = nm->mkNode(kind::BITVECTOR_PLUS, - nm->mkConst<BitVector>(BitVector( - utils::getSize(vvars[pcol]), rhs[prow])), + utils::mkConst( + utils::getSize(vvars[pcol]), rhs[prow]), tmp); } Assert(!is_bv_const(tmp)); |