Fix for bug 734

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 923e1d8c5f902809b5eff85ce653bfafb578e1dd..72f6dbfd13e74c329ec5ed78ad248db66d1fa47a 100644 (file)
--- 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 9607c02968e4a03d9d07d8785b241bc8519b5cfe..5fbdf74abe5ccbdfa3e50b78b155ca3b4a79d3be 100644 (file)
--- 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 b6b29410f84354c56179747b442c3b7a29724bfd..2fc5fd09686307bcd4ae0e0402fcfc07d7bc401a 100644 (file)
--- 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 2caaea7990264c941ad003d4234a86a527eab139..bb5c1e5878a34e8fcf913be2f9295218d6ba427d 100644 (file)
--- 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 (file)
index 0000000..1747c6c
--- /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)