From 9890b3bb5c2b81f26c9099577cb4bc939b1a9f47 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Fri, 31 May 2013 18:00:50 -0700
Subject: [PATCH] changing model format in duality to support boogie

---
 src/muz_qe/duality_dl_interface.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index 5922a8afd..eb455ffe7 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -307,7 +307,7 @@ void dl_interface::display_certificate(std::ostream& out) {
     local_func_decls = &locals;
     print_proof(this,out,_d->cex);
     out << ")\n";
-    out << "(model \n";
+    out << "(model \n\"";
     ::model mod(m_ctx.get_manager());
     model orig_model = _d->cex.tree->dualModel;
     for(unsigned i = 0; i < orig_model.num_consts(); i++){
@@ -325,7 +325,7 @@ void dl_interface::display_certificate(std::ostream& out) {
       }
     }
     model_v2_pp(out,mod);
-    out << ")\n";
+    out << "\")\n";
   }
 }