From: Dejan Jovanović Date: Sun, 10 Jun 2012 06:09:25 +0000 (+0000) Subject: adding an assertion to trigger the problem of bug349 and the testcase X-Git-Tag: cvc5-1.0.0~8094 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=103d6a6aad30410f8d7546c25c1f5e67f1c334d7;p=cvc5.git 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 0be232bfa..97c17222c 100644 --- 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 index 000000000..ab6abf7f5 --- /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 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))