1 files changed, 21 insertions, 0 deletions
diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index 4bd7b9d77..d2425831a 100644
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -81,4 +81,25 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format)
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out,
+                         theory::bv::BvOptimizeSatProof level)
+{
+  switch (level)
+  {
+    case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_NONE:
+      out << "BITVECTOR_OPTIMIZE_SAT_PROOF_NONE";
+      break;
+    case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF:
+      out << "BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF";
+      break;
+    case theory::bv::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA:
+      out << "BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA";
+      break;
+    default: out << "BvOptimizeSatProof:UNKNOWN![" << unsigned(level) << "]";
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
+