diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-05-17 18:42:13 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-17 18:42:13 +0000 |
| commit | 1703b160511396cd23be5203d9af86641b45766e (patch) | |
| tree | e1f085382022f853c068cef7990cd68fa3126f1b /src/printer/smt2 | |
| parent | a6f69a821e2d26f8901662193da5ee8dc74b158a (diff) | |
Fixed bug 338:
- fixed buggy rewrite rules assuming certain nodes only had 2 children
- added support for bv-rewrite dump
- fixed smt2_printer for bv constants
Diffstat (limited to 'src/printer/smt2')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2b686441a..25d3bf35a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -85,11 +85,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst<BitVector>(); const Integer& x = bv.getValue(); - out << "#b"; unsigned n = bv.getSize(); - while(n-- > 0) { - out << (x.testBit(n) ? '1' : '0'); - } + out << "(_ "; + out << "bv" << x <<" " << n; + out << ")"; + // //out << "#b"; + + // while(n-- > 0) { + // out << (x.testBit(n) ? '1' : '0'); + // } break; } case kind::CONST_BOOLEAN: |