From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Sep 2020 00:09:11 +0000 (-0500)
Subject: Add witness to cvc printer. (#5057)
X-Git-Tag: cvc5-1.0.0~2876
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=edf2e3ff7b751001901d377c3aacd044a3e15ef4;p=cvc5.git

Add witness to cvc printer. (#5057)
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2d59bff71..02afa715d 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -317,6 +317,13 @@ void CvcPrinter::toStream(
       out << ")";
       return;
       break;
+    case kind::WITNESS:
+      out << "(WITNESS";
+      toStream(out, n[0], depth, types, false);
+      out << " : ";
+      toStream(out, n[1], depth, types, false);
+      out << ')';
+      return;
     case kind::DISTINCT:
       // distinct not supported directly, blast it away with the rewriter
       toStream(out, theory::Rewriter::rewrite(n), depth, types, true);