From c356e6b4e5aecd6d13e398b361eb15a4dea18d91 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri, 2 Dec 2016 16:25:26 -0800
Subject: [PATCH] Fix for bug 734

---
 src/theory/bv/bv_inequality_graph.h     | 7 ++++---
 src/theory/bv/bv_subtheory_inequality.h | 4 ++--
 src/theory/bv/theory_bv.cpp             | 2 +-
 test/regress/regress0/bv/Makefile.am    | 1 +
 test/regress/regress0/bv/bug734.smt2    | 9 +++++++++
 5 files changed, 17 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/bv/bug734.smt2

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 923e1d8c5..72f6dbfd1 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -194,7 +194,8 @@ class InequalityGraph : public context::ContextNotifyObj{
   
   /*** The currently asserted disequalities */
   context::CDQueue<TNode> d_disequalities;
-  NodeSet d_disequalitiesAlreadySplit; 
+  typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+  CDNodeSet d_disequalitiesAlreadySplit; 
   Node makeDiseqSplitLemma(TNode diseq); 
   /** Backtracking mechanisms **/
   std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
@@ -208,7 +209,7 @@ class InequalityGraph : public context::ContextNotifyObj{
 
 public:
   
-  InequalityGraph(context::Context* c, bool s = false)
+  InequalityGraph(context::Context* c, context::Context* u, bool s = false)
     : ContextNotifyObj(c), 
       d_ineqNodes(),
       d_ineqEdges(),
@@ -216,7 +217,7 @@ public:
       d_conflict(),
       d_modelValues(c),
       d_disequalities(c),
-      d_disequalitiesAlreadySplit(),
+      d_disequalitiesAlreadySplit(u),
       d_undoStack(),
       d_undoStackIndex(c)
   {}
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 9607c0296..5fbdf74ab 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -53,10 +53,10 @@ class InequalitySolver: public SubtheorySolver {
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
   Statistics d_statistics;
 public:
-  InequalitySolver(context::Context* c, TheoryBV* bv)
+  InequalitySolver(context::Context* c, context::Context* u, TheoryBV* bv)
     : SubtheorySolver(c, bv),
       d_assertionSet(c),
-      d_inequalityGraph(c),
+      d_inequalityGraph(c, u),
       d_explanations(c),
       d_isComplete(c, true),
       d_ineqTerms(),
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b6b29410f..2fc5fd096 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -87,7 +87,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
   }
 
   if (options::bitvectorInequalitySolver()) {
-    SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
+    SubtheorySolver* ineq_solver = new InequalitySolver(c, u, this);
     d_subtheories.push_back(ineq_solver);
     d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
   }
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 2caaea799..bb5c1e587 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -113,6 +113,7 @@ BUG_TESTS = \
 	bug260a.smt \
 	bug260b.smt \
 	bug440.smt \
+	bug734.smt2 \
 	bug_extract_mult_leading_bit.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
diff --git a/test/regress/regress0/bv/bug734.smt2 b/test/regress/regress0/bv/bug734.smt2
new file mode 100644
index 000000000..1747c6cc4
--- /dev/null
+++ b/test/regress/regress0/bv/bug734.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x0 () (_ BitVec 3))
+(assert (not (= #b001 x0)))
+(assert (bvult #b000 x0))
+(check-sat)
+(check-sat)
-- 
2.30.2