summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.stanford.edu>2016-08-19 19:42:20 -0700
committerClark Barrett <barrett@cs.stanford.edu>2016-08-19 19:42:20 -0700
commit6b355496aaf27d46d6a33402814753589b755842 (patch)
tree93367699e064e0c081bdac42625b6d08b39e4fb8
parentd28f9f38ead8ec010a38e021f92d5de95261afc9 (diff)
Fixed two bugs
-rw-r--r--src/printer/cvc/cvc_printer.cpp2
-rw-r--r--src/smt/dump.cpp5
2 files changed, 4 insertions, 3 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index bc59e37ba..d09290db5 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -726,7 +726,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
case kind::BITVECTOR_SIGN_EXTEND:
out << "SX(";
toStream(out, n[0], depth, types, false);
- out << ", " << n.getOperator().getConst<BitVectorSignExtend>() << ')';
+ out << ", " << BitVectorType(n.getType().toType()).getSize() << ')';
return;
break;
case kind::BITVECTOR_ROTATE_LEFT:
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index eee7b901a..dc1ef792d 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -32,7 +32,9 @@ std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStrea
void DumpC::setDumpFromString(const std::string& optarg) {
#ifdef CVC4_DUMPING
- char* optargPtr = strdup(optarg.c_str());
+ // Make a copy of optarg for strtok_r to use.
+ std::string optargCopy = optarg;
+ char* optargPtr = const_cast<char*>(optargCopy.c_str());
char* tokstr = optargPtr;
char* toksave;
while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
@@ -130,7 +132,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
}
}
}
- free(optargPtr);
#else /* CVC4_DUMPING */
throw OptionException("The dumping feature was disabled in this build of CVC4.");
#endif /* CVC4_DUMPING */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback