Fixed two bugs

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index bc59e37ba9b1aeb0d15bea49465dd17263107199..d09290db58dffd0f2fb819ad54af00d68ed76de0 100644 (file)
--- 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 eee7b901ab28f4a6f40dbd50f764717d4c41349e..dc1ef792d53daff9ed54cb490728a4dd658440fe 100644 (file)
--- 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 */