From 95983dc012aa455b856f320ddcd4cfaf7c6a4582 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 12 Jul 2011 22:42:15 +0000 Subject: [PATCH] fix bug 272, array unsoundness, and some array cleanup --- src/theory/arrays/array_info.cpp | 38 ++--- src/theory/arrays/array_info.h | 6 +- src/theory/arrays/theory_arrays.cpp | 137 ++++++++++-------- src/theory/arrays/theory_arrays.h | 28 ++-- src/theory/arrays/theory_arrays_rewriter.h | 4 +- src/theory/rewriter.cpp | 4 +- src/theory/rewriter_attributes.h | 4 +- src/theory/theory.h | 4 +- src/theory/theory_engine.cpp | 18 +-- src/theory/theory_engine.h | 18 +-- ...nd1.minimized.smt => bug272.minimized.smt} | 0 .../arrays/{unsound1.smt => bug272.smt} | 0 12 files changed, 139 insertions(+), 122 deletions(-) rename test/regress/regress0/arrays/{unsound1.minimized.smt => bug272.minimized.smt} (100%) rename test/regress/regress0/arrays/{unsound1.smt => bug272.smt} (100%) diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index c795de0b9..5a836fdc2 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -34,20 +34,20 @@ bool inList(const CTNodeList* l, const TNode el) { void printList (CTNodeList* list) { CTNodeList::const_iterator it = list->begin(); - Debug("arrays-info")<<" [ "; + Trace("arrays-info")<<" [ "; for(; it != list->end(); it++ ) { - Debug("arrays-info")<<(*it)<<" "; + Trace("arrays-info")<<(*it)<<" "; } - Debug("arrays-info")<<"] \n"; + Trace("arrays-info")<<"] \n"; } void printList (List* list) { List::const_iterator it = list->begin(); - Debug("arrays-info")<<" [ "; + Trace("arrays-info")<<" [ "; for(; it != list->end(); it++ ) { - Debug("arrays-info")<<(*it)<<" "; + Trace("arrays-info")<<(*it)<<" "; } - Debug("arrays-info")<<"] \n"; + Trace("arrays-info")<<"] \n"; } void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ @@ -67,7 +67,7 @@ void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ void ArrayInfo::addIndex(const Node a, const TNode i) { Assert(a.getType().isArray()); Assert(!i.getType().isArray()); // temporary for flat arrays - Debug("arrays-ind")<<"Arrays::addIndex "<* temp_indices; Info* temp_info; @@ -84,7 +84,7 @@ void ArrayInfo::addIndex(const Node a, const TNode i) { temp_indices = (*it).second->indices; temp_indices->append(i); } - if(Debug.isOn("arrays-ind")) { + if(Trace.isOn("arrays-ind")) { printList((*(info_map.find(a))).second->indices); } @@ -115,7 +115,7 @@ void ArrayInfo::addStore(const Node a, const TNode st){ void ArrayInfo::addInStore(const TNode a, const TNode b){ - Debug("arrays-addinstore")<<"Arrays::addInStore "<print(); if(itb != info_map.end()) { - Debug("arrays-mergei")<<"Arrays::mergeInfo info "<print(); List* lista_i = (*ita).second->indices; @@ -241,9 +241,9 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ } } else { - Debug("arrays-mergei")<<" First element has no info \n"; + Trace("arrays-mergei")<<" First element has no info \n"; if(itb != info_map.end()) { - Debug("arrays-mergei")<<" adding second element's info \n"; + Trace("arrays-mergei")<<" adding second element's info \n"; (*itb).second->print(); List* listb_i = (*itb).second->indices; @@ -258,11 +258,11 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){ info_map[a] = temp_info; } else { - Debug("arrays-mergei")<<" Second element has no info \n"; + Trace("arrays-mergei")<<" Second element has no info \n"; } } - Debug("arrays-mergei")<<"Arrays::mergeInfo done \n"; + Trace("arrays-mergei")<<"Arrays::mergeInfo done \n"; } diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 6eb20e30a..ce3f015b5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -85,11 +85,11 @@ public: */ void print() const { Assert(indices != NULL && stores!= NULL); // && equals != NULL); - Debug("arrays-info")<<" indices "; + Trace("arrays-info")<<" indices "; printList(indices); - Debug("arrays-info")<<" stores "; + Trace("arrays-info")<<" stores "; printList(stores); - Debug("arrays-info")<<" in_stores "; + Trace("arrays-info")<<" in_stores "; printList(in_stores); } }; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index dab78c17a..888a98a45 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -76,7 +76,7 @@ TheoryArrays::~TheoryArrays() { void TheoryArrays::addSharedTerm(TNode t) { - Debug("arrays") << "Arrays::addSharedTerm(): " + Trace("arrays") << "Arrays::addSharedTerm(): " << t << endl; } @@ -85,7 +85,7 @@ void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { } void TheoryArrays::notifyCongruent(TNode a, TNode b) { - Debug("arrays") << "Arrays::notifyCongruent(): " + Trace("arrays") << "Arrays::notifyCongruent(): " << a << " = " << b << endl; if(!d_conflict.isNull()) { return; @@ -103,10 +103,10 @@ void TheoryArrays::check(Effort e) { return; } - Debug("arrays") <<"Arrays::start check "; + Trace("arrays") <<"Arrays::start check "; while(!done()) { Node assertion = get(); - Debug("arrays") << "Arrays::check(): " << assertion << endl; + Trace("arrays") << "Arrays::check(): " << assertion << endl; switch(assertion.getKind()) { case kind::EQUAL: @@ -143,6 +143,7 @@ void TheoryArrays::check(Effort e) { } else if(find(a) == find(b)) { Node conflict = constructConflict(assertion[0]); + d_conflict = Node::null(); d_out->conflict(conflict, false); return; } @@ -162,10 +163,10 @@ void TheoryArrays::check(Effort e) { // generate the lemmas on the worklist //while(!d_RowQueue.empty() || ! d_extQueue.empty()) { dischargeLemmas(); - Debug("arrays-lem")<<"Arrays::discharged lemmas "<mkNode(kind::SELECT, b, j); if(find(i) == find(j) || find(aj) == find(bj)) { - //Debug("arrays-lem")<<"isRedundantInContext valid "<mkConst(false); Node tt = nm->mkConst(true); if (literal1 == ff) { hasValue1 = true; satValue1 = false; - } - else if (literal1 == tt) { + } else if (literal1 == tt) { hasValue1 = true; satValue1 = true; + } else { + hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1)); } - else hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1)); if (hasValue1) { - if (satValue1) return true; - Node literal2 = Rewriter::rewrite(aj.eqNode(bj)); + if (satValue1) { + Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl; + return true; + } + Node ajeqbj = aj.eqNode(bj); + Node literal2 = Rewriter::rewrite(ajeqbj); bool hasValue2, satValue2; if (literal2 == ff) { hasValue2 = true; satValue2 = false; - } - else if (literal2 == tt) { + } else if (literal2 == tt) { hasValue2 = true; satValue2 = true; + } else { + hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2)); } - else hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2)); if (hasValue2) { - if (satValue2) return true; + if (satValue2) { + Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl; + return true; + } // conflict Assert(!satValue1 && !satValue2); Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL); NodeBuilder<2> nb(kind::AND); - literal1 = areDisequal(literal1[0],literal1[1]); - literal2 = areDisequal(literal2[0],literal2[1]); + //literal1 = areDisequal(literal1[0], literal1[1]); + //literal2 = areDisequal(literal2[0], literal2[1]); Assert(!literal1.isNull() && !literal2.isNull()); nb << literal1.notNode() << literal2.notNode(); literal1 = nb; + d_conflict = Node::null(); d_out->conflict(literal1, false); + Trace("arrays") << "TheoryArrays::isRedundantInContext() " + << "conflict via lemma: " << literal1 << endl; return true; } } - if(alreadyAddedRow(a,b,i,j)) { - // Debug("arrays-lem")<<"isRedundantInContext already added "<begin(); for( ; i!= (*it).second->end(); i++) { - Debug("arrays-prop")<<" "<<*i<<"\n"; + Trace("arrays-prop") << " " << *i << "\n"; TNode s = (*i)[0]; TNode t = (*i)[1]; @@ -791,12 +808,12 @@ TNode TheoryArrays::areDisequal(TNode a, TNode b) { } } - Debug("arrays-prop")<<" not disequal \n"; + Trace("arrays-prop") << " not disequal \n"; return TNode::null(); } bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { - Debug("arrays-prop")<<"Arrays::propagateFromRow "<mkNode(kind::SELECT, a, j); @@ -816,7 +833,7 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { // check if the current context implies that (NOT i = j) if(diseq != TNode::null()) { // if it's unassigned - Debug("arrays-prop")<<"satValue "<propagate(eq_aj_bj); ++d_numProp; @@ -848,14 +865,14 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { } } - Debug("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; + Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n"; return false; } void TheoryArrays::explain(TNode n) { - Debug("arrays")<<"Arrays::explain start for "<explanation(reason); - Debug("arrays")<<"explanation "<< reason<<" done \n"; + Trace("arrays")<<"explanation "<< reason<<" done \n"; */ } void TheoryArrays::checkRowLemmas(TNode a, TNode b) { - Debug("arrays-crl")<<"Arrays::checkLemmas begin \n"<print(); - Debug("arrays-crl")<<" ------------ and "<print(); List* i_a = d_infoMap.getIndices(a); @@ -995,7 +1012,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) { } } - Debug("arrays-crl")<<"Arrays::checkLemmas done.\n"; + Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } /** @@ -1018,7 +1035,7 @@ inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { - Debug("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lem); ++d_numRow; @@ -1032,10 +1049,10 @@ inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) { * store(a _ _ ) */ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { - Debug("arrays-cri")<<"Arrays::checkRowForIndex "<print(); } Assert(a.getType().isArray()); @@ -1048,9 +1065,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { TNode store = *it; Assert(store.getKind()==kind::STORE); TNode j = store[1]; - //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<print(); } Assert(a.getType().isArray()); @@ -1088,7 +1105,7 @@ void TheoryArrays::checkStore(TNode a) { TNode j = *it; if(!isRedundandRowLemma(a, b, i, j)) { - //Debug("arrays-lem")<<"Arrays::checkRowStore ("<mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk)); Node lem = nm->mkNode(kind::OR, eq, neq); - Debug("arrays-lem")<<"Arrays::addExtLemma "<lemma(lem); ++d_numExt; return; } - Debug("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index f4cccfec5..cf822cb65 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -260,7 +260,7 @@ private: bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) { - //Debug("arrays-lem")<<"alreadyAddedRow check for "<, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin(); a = find(a); b = find(b); @@ -274,7 +274,7 @@ private: TNode i_ = find((*it).third); TNode j_ = find((*it).fourth); if( a == a_ && b == b_ && i==i_ && j==j_) { - //Debug("arrays-lem")<<"alreadyAddedRow found "<getLevel()<<"\n"; + //Trace("arrays-preregister")<<"at level "<getLevel()<<"\n"; d_infoMap.addIndex(n[0], n[1]); checkRowForIndex(n[1], find(n[0])); - //Debug("arrays-preregister")<<"n[0] \n"; + //Trace("arrays-preregister")<<"n[0] \n"; //d_infoMap.getInfo(n[0])->print(); - //Debug("arrays-preregister")<<"find(n[0]) \n"; + //Trace("arrays-preregister")<<"find(n[0]) \n"; //d_infoMap.getInfo(find(n[0]))->print(); break; @@ -428,16 +428,16 @@ public: break; } default: - Debug("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; + Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n"; } } //void registerTerm(TNode n) { - // Debug("arrays-register")<<"Arrays::registerTerm "<::const_iterator it = d_prop_queue.begin(); /* @@ -466,10 +466,10 @@ public: for(; it!= d_atoms.end(); it++) { TNode eq = *it; Assert(eq.getKind()==kind::EQUAL); - Debug("arrays-prop")<<"value of "< rewriteStack; @@ -76,7 +76,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Get the top of the recursion stack RewriteStackElement& rewriteStackTop = rewriteStack.back(); - Debug("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl; + Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl; // Before rewriting children we need to do a pre-rewrite of the node if (rewriteStackTop.nextChild == 0) { diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index 86c2585b1..a2b2d06b7 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -51,7 +51,7 @@ struct RewriteAttibute { * Set the value of the pre-rewrite cache. */ static void setPreRewriteCache(TNode node, TNode cache) throw() { - Debug("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; + Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; Assert(!cache.isNull()); if (node == cache) { node.setAttribute(pre_rewrite(), Node::null()); @@ -83,7 +83,7 @@ struct RewriteAttibute { */ static void setPostRewriteCache(TNode node, TNode cache) throw() { Assert(!cache.isNull()); - Debug("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; + Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; if (node == cache) { node.setAttribute(post_rewrite(), Node::null()); } else { diff --git a/src/theory/theory.h b/src/theory/theory.h index 56a5f2f76..93d78f57c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -140,7 +140,7 @@ protected: TNode fact = d_facts[d_factsHead]; d_wasSharedTermFact = false; d_factsHead = d_factsHead + 1; - Debug("theory") << "Theory::get() => " << fact + Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; d_out->newFact(fact); return fact; @@ -312,7 +312,7 @@ public: * Assert a fact in the current context. */ void assertFact(TNode node) { - Debug("theory") << "Theory::assertFact(" << node << ")" << std::endl; + Trace("theory") << "Theory::assertFact(" << node << ")" << std::endl; d_facts.push_back(node); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3571171f8..28d7ab2c0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -73,7 +73,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { list toReg; toReg.push_back(fact); - Debug("theory") << "Theory::get(): registering new atom" << endl; + Trace("theory") << "Theory::get(): registering new atom" << endl; /* Essentially this is doing a breadth-first numbering of * non-registered subterms with children. Any non-registered @@ -195,20 +195,20 @@ void TheoryEngine::preRegister(TNode preprocessed) { } else { Theory* theory = theoryOf(current); TheoryId theoryLHS = theory->getId(); - Debug("register") << "preregistering " << current + Trace("register") << "preregistering " << current << " with " << theoryLHS << std::endl; markActive(theoryLHS); theory->preRegisterTerm(current); } } else { TheoryId theory = theoryIdOf(current); - Debug("register") << "preregistering " << current + Trace("register") << "preregistering " << current << " with " << theory << std::endl; markActive(theory); d_theoryTable[theory]->preRegisterTerm(current); TheoryId typeTheory = theoryIdOf(current.getType()); if (theory != typeTheory) { - Debug("register") << "preregistering " << current + Trace("register") << "preregistering " << current << " with " << typeTheory << std::endl; markActive(typeTheory); d_theoryTable[typeTheory]->preRegisterTerm(current); @@ -254,7 +254,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { try { CVC4_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { - Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; + Trace("theory") << "TheoryEngine::check() => conflict" << std::endl; } return true; @@ -315,7 +315,7 @@ bool TheoryEngine::presolve() { // Presolve for each theory using the statement above CVC4_FOR_EACH_THEORY; } catch(const theory::Interrupted&) { - Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; + Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl; } // return whether we have a conflict return !d_theoryOut.d_conflictNode.get().isNull(); @@ -374,9 +374,9 @@ bool TheoryEngine::hasRegisterTerm(TheoryId th) const { theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - Debug("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; + Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut); - Debug("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; + Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; return solveStatus; } @@ -390,7 +390,7 @@ struct preprocess_stack_element { Node TheoryEngine::preprocess(TNode assertion) { - Debug("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; + Trace("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; // Do a topological sort of the subexpressions and substitute them vector toVisit; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d4138f807..3507723f9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -126,7 +126,7 @@ class TheoryEngine { void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::conflict(" + Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; ++(d_engine->d_statistics.d_statConflicts); @@ -137,7 +137,7 @@ class TheoryEngine { void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::propagate(" + Trace("theory") << "EngineOutputChannel::propagate(" << lit << ")" << std::endl; d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); @@ -145,7 +145,7 @@ class TheoryEngine { void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::lemma(" + Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); @@ -153,7 +153,7 @@ class TheoryEngine { void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::explanation(" + Trace("theory") << "EngineOutputChannel::explanation(" << explanationNode << ")" << std::endl; d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); @@ -355,7 +355,7 @@ public: * @param node the assertion */ inline void assertFact(TNode node) { - Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; // Mark it as asserted in this context // @@ -369,16 +369,16 @@ public: // Again, equality is a special case if (atom.getKind() == kind::EQUAL) { if(d_logic == "QF_AX") { - Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; + Trace("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; d_theoryTable[theory::THEORY_ARRAY]->assertFact(node); } else { theory::Theory* theory = theoryOf(atom); - Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; + Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl; theory->assertFact(node); } } else { theory::Theory* theory = theoryOf(atom); - Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; + Trace("theory") << "asserting " << node << " to " << theory->getId() << std::endl; theory->assertFact(node); } } @@ -443,7 +443,7 @@ public: TNode atom = node.getKind() == kind::NOT ? node[0] : node; if (atom.getKind() == kind::EQUAL) { if(d_logic == "QF_AX") { - Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; + Trace("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl; d_theoryTable[theory::THEORY_ARRAY]->explain(node); } else { theoryOf(atom[0])->explain(node); diff --git a/test/regress/regress0/arrays/unsound1.minimized.smt b/test/regress/regress0/arrays/bug272.minimized.smt similarity index 100% rename from test/regress/regress0/arrays/unsound1.minimized.smt rename to test/regress/regress0/arrays/bug272.minimized.smt diff --git a/test/regress/regress0/arrays/unsound1.smt b/test/regress/regress0/arrays/bug272.smt similarity index 100% rename from test/regress/regress0/arrays/unsound1.smt rename to test/regress/regress0/arrays/bug272.smt -- 2.30.2