From f7d589fc49d1ed30761705732dcfaf7338777085 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Thu, 10 Apr 2014 17:53:00 -0700
Subject: [PATCH] changed fixedpoint output format for easier parsing in Boogie

---
 src/muz/duality/duality_dl_interface.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 587a184bc..99ac2ee1c 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -350,7 +350,9 @@ void dl_interface::display_certificate_non_const(std::ostream& out) {
   if(_d->status == StatusModel){
     ast_manager &m = m_ctx.get_manager();
     model_ref md = get_model();
+    out << "(fixedpoint \n";
     model_smt2_pp(out, m, *md.get(), 0); 
+    out << ")\n";
   }
   else if(_d->status == StatusRefutation){
     out << "(derivation\n";