adding an assertion to trigger the problem of bug349 and the testcase

bv rewriter apparently deosn't have a proper normal form for equalities

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0be232bfa756d81593f8306a858544f56c2ec91a..97c17222c56da40649d75a230c327c63698b3418 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -444,6 +444,11 @@ bool TheoryEngine::properConflict(TNode conflict) const {
                                 << conflict[i] << endl;
         return false;
       }
+      if (conflict[i] != Rewriter::rewrite(conflict[i])) {
+        Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
+                                << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
+        return false;
+      }
     }
   } else {
     if (! getPropEngine()->hasValue(conflict, value)) {
@@ -456,6 +461,11 @@ bool TheoryEngine::properConflict(TNode conflict) const {
                               << conflict << endl;
       return false;
     }
+    if (conflict != Rewriter::rewrite(conflict)) {
+      Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
+                              << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
+      return false;
+    }
   }
   return true;
 }
@@ -1094,6 +1104,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     getExplanation(explanationVector);
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << std::endl;
+    Assert(properConflict(fullConflict));
     lemma(fullConflict, true, false);
   } else {
     // When only one theory, the conflict should need no processing

diff --git a/test/regress/regress0/aufbv/bug349.smt b/test/regress/regress0/aufbv/bug349.smt
new file mode 100644 (file)
index 0000000..ab6abf7
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug349.smt
@@ -0,0 +1,134 @@
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((start2 BitVec[32]))
+:extrafuns ((start1 BitVec[32]))
+:extrafuns ((a1 Array[32:8]))
+:status unsat
+:formula
+(let (?n1 bv0[1])
+(let (?n2 bv0[8])
+(let (?n3 (store a1 start1 ?n2))
+(let (?n4 bv3[32])
+(let (?n5 (bvadd ?n4 start1))
+(let (?n6 (store ?n3 ?n5 ?n2))
+(let (?n7 bv1[32])
+(let (?n8 (select ?n6 ?n7))
+(let (?n9 (bvnot ?n8))
+(let (?n10 bv0[32])
+(let (?n11 (select ?n6 ?n10))
+(let (?n12 (bvnot ?n11))
+(let (?n13 (bvand ?n9 ?n12))
+(let (?n14 (bvnot ?n13))
+(let (?n15 (bvand ?n8 ?n11))
+(let (?n16 (bvnot ?n15))
+(let (?n17 (bvand ?n14 ?n16))
+(let (?n18 (bvnot ?n17))
+(let (?n19 (bvand ?n9 ?n18))
+(let (?n20 (bvnot ?n19))
+(let (?n21 (bvand ?n8 ?n17))
+(let (?n22 (bvnot ?n21))
+(let (?n23 (bvand ?n20 ?n22))
+(let (?n24 (store ?n6 ?n7 ?n23))
+(let (?n25 (bvnot ?n23))
+(let (?n26 (bvand ?n18 ?n25))
+(let (?n27 (bvnot ?n26))
+(let (?n28 (bvand ?n17 ?n23))
+(let (?n29 (bvnot ?n28))
+(let (?n30 (bvand ?n27 ?n29))
+(let (?n31 (store ?n24 ?n10 ?n30))
+(let (?n32 (bvadd ?n4 start2))
+(let (?n33 (select ?n31 ?n32))
+(let (?n34 (bvnot ?n33))
+(let (?n35 (select ?n31 start2))
+(let (?n36 (bvnot ?n35))
+(let (?n37 (bvand ?n34 ?n36))
+(let (?n38 (bvnot ?n37))
+(let (?n39 (bvand ?n33 ?n35))
+(let (?n40 (bvnot ?n39))
+(let (?n41 (bvand ?n38 ?n40))
+(let (?n42 (bvnot ?n41))
+(let (?n43 (bvand ?n34 ?n42))
+(let (?n44 (bvnot ?n43))
+(let (?n45 (bvand ?n33 ?n41))
+(let (?n46 (bvnot ?n45))
+(let (?n47 (bvand ?n44 ?n46))
+(let (?n48 (store ?n31 ?n32 ?n47))
+(let (?n49 (bvnot ?n47))
+(let (?n50 (bvand ?n42 ?n49))
+(let (?n51 (bvnot ?n50))
+(let (?n52 (bvand ?n41 ?n47))
+(let (?n53 (bvnot ?n52))
+(let (?n54 (bvand ?n51 ?n53))
+(let (?n55 (store ?n48 start2 ?n54))
+(let (?n56 (select ?n55 ?n10))
+(let (?n57 (bvnot ?n56))
+(let (?n58 (select ?n55 start2))
+(let (?n59 (bvnot ?n58))
+(let (?n60 (bvand ?n57 ?n59))
+(let (?n61 (bvnot ?n60))
+(let (?n62 (bvand ?n56 ?n58))
+(let (?n63 (bvnot ?n62))
+(let (?n64 (bvand ?n61 ?n63))
+(let (?n65 (bvnot ?n64))
+(let (?n66 (bvand ?n57 ?n65))
+(let (?n67 (bvnot ?n66))
+(let (?n68 (bvand ?n56 ?n64))
+(let (?n69 (bvnot ?n68))
+(let (?n70 (bvand ?n67 ?n69))
+(let (?n71 (store ?n55 ?n10 ?n70))
+(let (?n72 (bvnot ?n70))
+(let (?n73 (bvand ?n65 ?n72))
+(let (?n74 (bvnot ?n73))
+(let (?n75 (bvand ?n64 ?n70))
+(let (?n76 (bvnot ?n75))
+(let (?n77 (bvand ?n74 ?n76))
+(let (?n78 (store ?n71 start2 ?n77))
+(let (?n79 (select ?n78 ?n7))
+(let (?n80 (bvnot ?n79))
+(let (?n81 (select ?n78 ?n10))
+(let (?n82 (bvnot ?n81))
+(let (?n83 (bvand ?n80 ?n82))
+(let (?n84 (bvnot ?n83))
+(let (?n85 (bvand ?n79 ?n81))
+(let (?n86 (bvnot ?n85))
+(let (?n87 (bvand ?n84 ?n86))
+(let (?n88 (bvnot ?n87))
+(let (?n89 (bvand ?n80 ?n88))
+(let (?n90 (bvnot ?n89))
+(let (?n91 (bvand ?n79 ?n87))
+(let (?n92 (bvnot ?n91))
+(let (?n93 (bvand ?n90 ?n92))
+(let (?n94 (store ?n78 ?n7 ?n93))
+(let (?n95 (bvnot ?n93))
+(let (?n96 (bvand ?n88 ?n95))
+(let (?n97 (bvnot ?n96))
+(let (?n98 (bvand ?n87 ?n93))
+(let (?n99 (bvnot ?n98))
+(let (?n100 (bvand ?n97 ?n99))
+(let (?n101 (store ?n94 ?n10 ?n100))
+(let (?n102 (store a1 ?n5 ?n2))
+(let (?n103 (store ?n102 start1 ?n2))
+(let (?n104 (select ?n103 ?n10))
+(let (?n105 (store ?n103 ?n7 ?n104))
+(let (?n106 (select ?n103 ?n7))
+(let (?n107 (store ?n105 ?n10 ?n106))
+(let (?n108 (select ?n107 start2))
+(let (?n109 (store ?n107 ?n32 ?n108))
+(let (?n110 (select ?n107 ?n32))
+(let (?n111 (store ?n109 start2 ?n110))
+(let (?n112 (select ?n111 start2))
+(let (?n113 (store ?n111 ?n10 ?n112))
+(let (?n114 (select ?n111 ?n10))
+(let (?n115 (store ?n113 start2 ?n114))
+(let (?n116 (select ?n115 ?n10))
+(let (?n117 (store ?n115 ?n7 ?n116))
+(let (?n118 (select ?n115 ?n7))
+(let (?n119 (store ?n117 ?n10 ?n118))
+(flet ($n120 (= ?n101 ?n119))
+(let (?n121 bv1[1])
+(let (?n122 (ite $n120 ?n121 ?n1))
+(let (?n123 (bvnot ?n122))
+(flet ($n124 (= ?n1 ?n123))
+(flet ($n125 (not $n124))
+$n125
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))