diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala index f77c7519c..9e7b6e682 100644 --- a/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala +++ b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala @@ -24,7 +24,6 @@ trait CVC4Solver extends SMTLIBSolver with CVC4Target { "--produce-models", "--incremental", // "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs - "--rewrite-divk", "--print-success", "--lang", "smt2.5" ) ++ options.findOptionOrDefault(optCVC4Options) diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala index 95e146c21..05d743275 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala +++ b/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala @@ -81,15 +81,20 @@ trait SMTLIBParser { case _ => IntegerLiteral(n) } - case FixedSizeBitVectors.BitVectorLit(bs) => otpe match { - case Some(BVType(signed, _)) => - BVLiteral(signed, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size) - case _ => - BVLiteral(true, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size) - } + case FixedSizeBitVectors.BitVectorLit(bs) => + otpe match { + case Some(BVType(signed, _)) => + BVLiteral(signed, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size) + case Some(CharType()) => + val bv = BVLiteral(true, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, 16) + CharLiteral(bv.toBigInt.toInt.toChar) + case _ => + BVLiteral(true, BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size) + } case FixedSizeBitVectors.BitVectorConstant(n, size) => otpe match { case Some(BVType(signed, _)) => BVLiteral(signed, n, size.intValue) + case Some(CharType()) => CharLiteral(n.toChar) case _ => BVLiteral(true, n, size.intValue) } diff --git a/src/main/scala/inox/utils/ASCIIHelpers.scala b/src/main/scala/inox/utils/ASCIIHelpers.scala index e8a576216..79a2e126d 100644 --- a/src/main/scala/inox/utils/ASCIIHelpers.scala +++ b/src/main/scala/inox/utils/ASCIIHelpers.scala @@ -72,23 +72,23 @@ object ASCIIHelpers { val sb = new StringBuffer - val barH = if (asciiOnly) "#" else "─" - val topLeft = if (asciiOnly) "#" else "┌" - val topRight = if (asciiOnly) "#" else "┐" - val bottomLeft = if (asciiOnly) "#" else "└" - val bottomRight = if (asciiOnly) "#" else "┘" + val barH = if (asciiOnly) "" else "─" + val topLeft = if (asciiOnly) "" else "┌" + val topRight = if (asciiOnly) "" else "┐" + val bottomLeft = if (asciiOnly) "" else "└" + val bottomRight = if (asciiOnly) "" else "┘" val dots = if (asciiOnly) "." else "┄" - val doubleBarH = if (asciiOnly) "#" else "═" - val doubleBarV = if (asciiOnly) "#" else "║" - val doubleTopLeft = if (asciiOnly) "#" else "╔" - val doubleTopRight = if (asciiOnly) "#" else "╗" - val doubleBottomLeft = if (asciiOnly) "#" else "╚" - val doubleBottomRight = if (asciiOnly) "#" else "╝" - - val leftConnect = if (asciiOnly) "#" else "╡" - val rightConnect = if (asciiOnly) "#" else "╞" - val doubleRightConnect = if (asciiOnly) "#" else "╟" - val doubleLeftConnect = if (asciiOnly) "#" else "╢" + val doubleBarH = if (asciiOnly) "" else "═" + val doubleBarV = if (asciiOnly) "" else "║" + val doubleTopLeft = if (asciiOnly) "" else "╔" + val doubleTopRight = if (asciiOnly) "" else "╗" + val doubleBottomLeft = if (asciiOnly) "" else "╚" + val doubleBottomRight = if (asciiOnly) "" else "╝" + + val leftConnect = if (asciiOnly) "" else "╡" + val rightConnect = if (asciiOnly) "" else "╞" + val doubleRightConnect = if (asciiOnly) "" else "╟" + val doubleLeftConnect = if (asciiOnly) "" else "╢" sb append s" $topLeft$barH" + (barH * titleWidth) + s"$barH$topRight\n" sb append s"$doubleTopLeft$doubleBarH$leftConnect " + title + s" $rightConnect" + (doubleBarH * padWidth) + s"$doubleTopRight\n" @@ -99,7 +99,7 @@ object ASCIIHelpers { sb append doubleRightConnect + (dots * fullWidth) + s"$doubleLeftConnect\n" case Row(cells) => - sb append s"$doubleBarV " + if (!asciiOnly) sb append s"$doubleBarV " var i = 0 for (c <- cells) { if (i > 0) {