From ca381589665c3888a9e4c35849826b755036249a Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Fri, 31 May 2013 17:52:51 -0700
Subject: [PATCH] fix bug in getting decision count in duality

---
 src/duality/duality_wrapper.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index bfdc382bf..fcb637a84 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -296,6 +296,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     st.display(ss);
     std::string stats = ss.str();
     int pos = stats.find("decisions:");
+    if(pos < 0) return 0; // for some reason, decisions are not reported if there are none
     pos += 10;
     int end = stats.find('\n',pos);
     std::string val = stats.substr(pos,end-pos);