From 9cd7b9b4f657b15b4eaf80c45284a696647697c1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 Oct 2016 22:13:23 -0700
Subject: [PATCH] fix mutex finding for smt-core: it was returning mutexes for
 negations of literals

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_consequences.cpp      |  2 +-
 src/tactic/arith/pb2bv_tactic.cpp | 21 ++++++++++++++-------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index e44782a31..ef90aac4c 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -373,7 +373,7 @@ namespace smt {
             expr* n = vars[i];
             bool neg = m_manager.is_not(n, n);
             if (b_internalized(n)) {
-                lits.insert(literal(get_bool_var(n), !neg).index());
+                lits.insert(literal(get_bool_var(n), neg).index());
             }
         }
         while (!lits.empty()) {
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 4c3790af3..6348ddd74 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -29,10 +29,11 @@ Notes:
 #include"filter_model_converter.h"
 #include"pb2bv_model_converter.h"
 #include"pb2bv_tactic.h"
+#include"ast_pp.h"
 
 class pb2bv_tactic : public tactic {
 public:
-    struct non_pb {};
+    struct non_pb { expr* e; non_pb(expr* e) : e(e) {}};
 
     struct only_01_visitor {
         typedef rational numeral;
@@ -48,7 +49,7 @@ public:
     
         void throw_non_pb(expr * n) {
             TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";);
-            throw non_pb();
+            throw non_pb(n);
         }
     
         void operator()(var * n) { 
@@ -575,7 +576,7 @@ private:
     
         void throw_non_pb(expr * n) {        
             TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";);
-            throw non_pb();
+            throw non_pb(n);
         }
 
         // check if polynomial is encoding 
@@ -910,8 +911,8 @@ private:
             try {
                 quick_pb_check(g);
             }
-            catch (non_pb) {
-                throw tactic_exception("goal is in a fragment unsupported by pb2bv");
+            catch (non_pb& p) {
+                throw_tactic(p.e);
             }
                         
             unsigned size = g->size();
@@ -940,8 +941,8 @@ private:
                     new_exprs.push_back(new_f);
                 }                
             }
-            catch (non_pb) {
-                throw tactic_exception("goal is in a fragment unsupported by pb2bv");
+            catch (non_pb& p) {
+                throw_tactic(p.e);
             }
 
             for (unsigned idx = 0; idx < size; idx++)
@@ -966,6 +967,12 @@ private:
             TRACE("pb2bv", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
+
+        void throw_tactic(expr* e) {
+            std::stringstream strm;
+            strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m);
+            throw tactic_exception(strm.str().c_str());
+        }
     };
 
     imp *      m_imp;