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/lazy_bitblaster.cpp | |
| parent | 215c41d35390927409aac3827798f89d82f6b4bb (diff) | |
Add bv util mkConst(unsigned, Integer&). (#1499)
Diffstat (limited to 'src/theory/bv/lazy_bitblaster.cpp')
| -rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 7976097e1..831b767e0 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -481,7 +481,7 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); value = value * 2 + bit_int; } - return utils::mkConst(BitVector(bits.size(), value)); + return utils::mkConst(bits.size(), value); } bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) |