From 0ff21bf1d615500ca135f36f5ec8c57c1fd47438 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 16 May 2013 16:54:20 -0500 Subject: Fix minor bug in full_model_check.cpp --- src/theory/quantifiers/full_model_check.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 445f0d6c0..c2a3f895b 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -163,7 +163,7 @@ void Def::simplify(FullModelChecker * m) { d_et.reset(); for (unsigned i=0; i Date: Thu, 16 May 2013 18:55:08 -0400 Subject: configure fix for building with glpk on redhat, perhaps others --- config/glpk.m4 | 18 ++++++++++++++---- src/theory/arith/approx_simplex.cpp | 10 ++++++++-- 2 files changed, 22 insertions(+), 6 deletions(-) (limited to 'src/theory') diff --git a/config/glpk.m4 b/config/glpk.m4 index 7380ad0e2..6c59a3094 100644 --- a/config/glpk.m4 +++ b/config/glpk.m4 @@ -13,8 +13,10 @@ elif test "$with_glpk" = yes; then dnl Try a bunch of combinations until something works :-/ GLPK_LIBS= - AC_CHECK_HEADER([glpk.h], [], - [AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!])]) + AC_CHECK_HEADERS([glpk/glpk.h glpk.h], [break]) + if test x$ac_cv_header_glpk_glpk_h = xno && test x$ac_cv_header_glpk_h = xno; then + AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!]) + fi AC_MSG_CHECKING([how to link glpk]) CVC4_TRY_GLPK_WITH([]) CVC4_TRY_GLPK_WITH([-lgmp]) @@ -88,7 +90,11 @@ if test -z "$GLPK_LIBS"; then AC_LANG_PUSH([C++]) cvc4_save_LIBS="$LIBS" LIBS="-lglpk $1" - AC_LINK_IFELSE([AC_LANG_PROGRAM([#include ], + AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H] + [#include ] + [#else] + [#include ] + [#endif], [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])], [GLPK_LIBS="-lglpk $1"], []) @@ -107,7 +113,11 @@ if test -z "$GLPK_LIBS"; then cvc4_save_LDFLAGS="$LDFLAGS" LDFLAGS="-static $LDFLAGS" LIBS="-lglpk $1" - AC_LINK_IFELSE([AC_LANG_PROGRAM([#include ], + AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H] + [#include ] + [#else] + [#include ] + [#endif], [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])], [GLPK_LIBS="-lglpk $1"], []) diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 47f15d8c7..0f5a0fd4e 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -116,8 +116,14 @@ public: /* Begin the declaration of GLPK specific code. */ #ifdef CVC4_USE_GLPK extern "C" { -#include -} +/* Sometimes the header is in a subdirectory glpk/, sometimes not. + * The configure script figures it out. */ +#ifdef HAVE_GLPK_GLPK_H +# include +#else /* HAVE_GLPK_GLPK_H */ +# include +#endif /* HAVE_GLPK_GLPK_H */ +}/* extern "C" */ namespace CVC4 { namespace theory { -- cgit v1.2.3 From d6ef5385a8759d708b75077ec7e919eff783a6cf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 10:19:54 -0400 Subject: Better error on invalid logic strings. Thanks to David Cok for reporting this issue. --- library_versions | 1 + src/smt/smt_engine.cpp | 16 ++++++++-------- src/smt/smt_engine.h | 4 ++-- src/theory/logic_info.cpp | 7 ++++++- 4 files changed, 17 insertions(+), 11 deletions(-) (limited to 'src/theory') diff --git a/library_versions b/library_versions index eac360c34..7174f7b0b 100644 --- a/library_versions +++ b/library_versions @@ -53,3 +53,4 @@ 1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.3-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 +# note: SmtEngine::setLogicString() exceptions have changed, bump library version on next release? diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 908ad05e2..ab4b13d4c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -792,21 +792,21 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { SmtScope smts(this); - d_logic = logic; setLogicInternal(); } -void SmtEngine::setLogic(const std::string& s) throw(ModalException) { +void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicException) { SmtScope smts(this); - - setLogic(LogicInfo(s)); + try { + setLogic(LogicInfo(s)); + } catch(IllegalArgumentException& e) { + throw LogicException(e.what()); + } } -void SmtEngine::setLogic(const char* logic) throw(ModalException){ - SmtScope smts(this); - - setLogic(LogicInfo(string(logic))); +void SmtEngine::setLogic(const char* logic) throw(ModalException, LogicException) { + setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a22e34c21..8266bb1ed 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -350,12 +350,12 @@ public: /** * Set the logic of the script. */ - void setLogic(const std::string& logic) throw(ModalException); + void setLogic(const std::string& logic) throw(ModalException, LogicException); /** * Set the logic of the script. */ - void setLogic(const char* logic) throw(ModalException); + void setLogic(const char* logic) throw(ModalException, LogicException); /** * Set the logic of the script. diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index dc9de8662..cbd0b510e 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -241,7 +241,12 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } if(*p != '\0') { stringstream err; - err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString; + err << "LogicInfo::setLogicString(): "; + if(p == logicString) { + err << "cannot parse logic string: " << logicString; + } else { + err << "junk (\"" << p << "\") at end of logic string: " << logicString; + } IllegalArgument(logicString, err.str().c_str()); } -- cgit v1.2.3 From 01654ea86af49fdf0859811f09c64de66dcc9f59 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 10 May 2013 13:01:02 -0400 Subject: Fix erroneous results when the logic was incorrectly specified (by throwing LogicException). Also correct a case where sharing was doing some work during pure theory solving. --- src/theory/term_registration_visitor.cpp | 9 --------- src/theory/term_registration_visitor.h | 15 ++++----------- src/theory/theory_engine.cpp | 20 +++++++++++++++++++- 3 files changed, 23 insertions(+), 21 deletions(-) (limited to 'src/theory') diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 48d00130c..558975a72 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -127,15 +127,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { Assert(alreadyVisited(current, parent)); } -void PreRegisterVisitor::start(TNode node) { - d_multipleTheories = false; -} - -bool PreRegisterVisitor::done(TNode node) { - // We have multiple theories if removing the node theory from others is non-empty - return Theory::setRemove(Theory::theoryOf(node), d_theories); -} - std::string SharedTermsVisitor::toString() const { std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 768508d2c..478e82d19 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -54,11 +54,6 @@ class PreRegisterVisitor { */ theory::Theory::Set d_theories; - /** - * Is true if the term we're traversing involves multiple theories. - */ - bool d_multipleTheories; - /** * String representation of the visited map, for debugging purposes. */ @@ -66,14 +61,13 @@ class PreRegisterVisitor { public: - /** Return type tells us if there are more than one theory or not */ - typedef bool return_type; + /** Returned set tells us which theories there are */ + typedef theory::Theory::Set return_type; PreRegisterVisitor(TheoryEngine* engine, context::Context* context) : d_engine(engine) , d_visited(context) , d_theories(0) - , d_multipleTheories(false) {} /** @@ -89,13 +83,12 @@ public: /** * Marks the node as the starting literal. */ - void start(TNode node); + void start(TNode node) { } /** * Notifies the engine of all the theories used. */ - bool done(TNode node); - + theory::Theory::Set done(TNode node) { return d_theories; } }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a81b38fe9..5ee8e5fda 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -187,7 +187,25 @@ void TheoryEngine::preRegister(TNode preprocessed) { } // Pre-register the terms in the atom - bool multipleTheories = NodeVisitor::run(d_preRegistrationVisitor, preprocessed); + Theory::Set theories = NodeVisitor::run(d_preRegistrationVisitor, preprocessed); + theories = Theory::setRemove(THEORY_BOOL, theories); + // Remove the top theory, if any more that means multiple theories were involved + bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories); + TheoryId i; + while((i = Theory::setPop(theories)) != THEORY_LAST) { + if(!d_logicInfo.isTheoryEnabled(i)) { + LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy(); + newLogicInfo.enableTheory(i); + newLogicInfo.lock(); + stringstream ss; + ss << "The logic was specified as " << d_logicInfo.getLogicString() + << ", which doesn't include " << i + << ", but found a term in that theory." << endl + << "You might want to extend your logic to " << newLogicInfo + << endl; + throw LogicException(ss.str()); + } + } if (multipleTheories) { // Collect the shared terms if there are multipe theories NodeVisitor::run(d_sharedTermsVisitor, preprocessed); -- cgit v1.2.3 From 10bc76f38b5fa7d213f698fa7b8de14d20e40c07 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 10 May 2013 17:08:23 -0400 Subject: disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not) --- src/theory/theory_engine.cpp | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) (limited to 'src/theory') diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5ee8e5fda..ee37f331e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -192,18 +192,23 @@ void TheoryEngine::preRegister(TNode preprocessed) { // Remove the top theory, if any more that means multiple theories were involved bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories); TheoryId i; - while((i = Theory::setPop(theories)) != THEORY_LAST) { - if(!d_logicInfo.isTheoryEnabled(i)) { - LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy(); - newLogicInfo.enableTheory(i); - newLogicInfo.lock(); - stringstream ss; - ss << "The logic was specified as " << d_logicInfo.getLogicString() - << ", which doesn't include " << i - << ", but found a term in that theory." << endl - << "You might want to extend your logic to " << newLogicInfo - << endl; - throw LogicException(ss.str()); + // These checks don't work with finite model finding, because it + // uses Rational constants to represent cardinality constraints, + // even though arithmetic isn't actually involved. + if(!options::finiteModelFind()) { + while((i = Theory::setPop(theories)) != THEORY_LAST) { + if(!d_logicInfo.isTheoryEnabled(i)) { + LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy(); + newLogicInfo.enableTheory(i); + newLogicInfo.lock(); + stringstream ss; + ss << "The logic was specified as " << d_logicInfo.getLogicString() + << ", which doesn't include " << i + << ", but found a term in that theory." << endl + << "You might want to extend your logic to " + << newLogicInfo.getLogicString() << endl; + throw LogicException(ss.str()); + } } } if (multipleTheories) { -- cgit v1.2.3 From 67cd7748e776bcceefe7b06edcfc316876cca9bd Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 16 May 2013 18:55:08 -0400 Subject: configure fix for building with glpk on redhat, perhaps others --- config/glpk.m4 | 18 ++++++++++++++---- src/theory/arith/approx_simplex.cpp | 10 ++++++++-- 2 files changed, 22 insertions(+), 6 deletions(-) (limited to 'src/theory') diff --git a/config/glpk.m4 b/config/glpk.m4 index 7380ad0e2..6c59a3094 100644 --- a/config/glpk.m4 +++ b/config/glpk.m4 @@ -13,8 +13,10 @@ elif test "$with_glpk" = yes; then dnl Try a bunch of combinations until something works :-/ GLPK_LIBS= - AC_CHECK_HEADER([glpk.h], [], - [AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!])]) + AC_CHECK_HEADERS([glpk/glpk.h glpk.h], [break]) + if test x$ac_cv_header_glpk_glpk_h = xno && test x$ac_cv_header_glpk_h = xno; then + AC_MSG_FAILURE([cannot find glpk.h, the GLPK header!]) + fi AC_MSG_CHECKING([how to link glpk]) CVC4_TRY_GLPK_WITH([]) CVC4_TRY_GLPK_WITH([-lgmp]) @@ -88,7 +90,11 @@ if test -z "$GLPK_LIBS"; then AC_LANG_PUSH([C++]) cvc4_save_LIBS="$LIBS" LIBS="-lglpk $1" - AC_LINK_IFELSE([AC_LANG_PROGRAM([#include ], + AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H] + [#include ] + [#else] + [#include ] + [#endif], [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])], [GLPK_LIBS="-lglpk $1"], []) @@ -107,7 +113,11 @@ if test -z "$GLPK_LIBS"; then cvc4_save_LDFLAGS="$LDFLAGS" LDFLAGS="-static $LDFLAGS" LIBS="-lglpk $1" - AC_LINK_IFELSE([AC_LANG_PROGRAM([#include ], + AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H] + [#include ] + [#else] + [#include ] + [#endif], [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])], [GLPK_LIBS="-lglpk $1"], []) diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 47f15d8c7..0f5a0fd4e 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -116,8 +116,14 @@ public: /* Begin the declaration of GLPK specific code. */ #ifdef CVC4_USE_GLPK extern "C" { -#include -} +/* Sometimes the header is in a subdirectory glpk/, sometimes not. + * The configure script figures it out. */ +#ifdef HAVE_GLPK_GLPK_H +# include +#else /* HAVE_GLPK_GLPK_H */ +# include +#endif /* HAVE_GLPK_GLPK_H */ +}/* extern "C" */ namespace CVC4 { namespace theory { -- cgit v1.2.3 From 59cb1ace343f74af41fae55933be48d1b3995780 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 10:19:54 -0400 Subject: Better error on invalid logic strings. Thanks to David Cok for reporting this issue. Conflicts: library_versions --- src/smt/smt_engine.cpp | 16 ++++++++-------- src/smt/smt_engine.h | 4 ++-- src/theory/logic_info.cpp | 7 ++++++- 3 files changed, 16 insertions(+), 11 deletions(-) (limited to 'src/theory') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 284f39d54..3ee6b1d74 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -791,21 +791,21 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { SmtScope smts(this); - d_logic = logic; setLogicInternal(); } -void SmtEngine::setLogic(const std::string& s) throw(ModalException) { +void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicException) { SmtScope smts(this); - - setLogic(LogicInfo(s)); + try { + setLogic(LogicInfo(s)); + } catch(IllegalArgumentException& e) { + throw LogicException(e.what()); + } } -void SmtEngine::setLogic(const char* logic) throw(ModalException){ - SmtScope smts(this); - - setLogic(LogicInfo(string(logic))); +void SmtEngine::setLogic(const char* logic) throw(ModalException, LogicException) { + setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a22e34c21..8266bb1ed 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -350,12 +350,12 @@ public: /** * Set the logic of the script. */ - void setLogic(const std::string& logic) throw(ModalException); + void setLogic(const std::string& logic) throw(ModalException, LogicException); /** * Set the logic of the script. */ - void setLogic(const char* logic) throw(ModalException); + void setLogic(const char* logic) throw(ModalException, LogicException); /** * Set the logic of the script. diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index dc9de8662..cbd0b510e 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -241,7 +241,12 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } if(*p != '\0') { stringstream err; - err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString; + err << "LogicInfo::setLogicString(): "; + if(p == logicString) { + err << "cannot parse logic string: " << logicString; + } else { + err << "junk (\"" << p << "\") at end of logic string: " << logicString; + } IllegalArgument(logicString, err.str().c_str()); } -- cgit v1.2.3 From 48d863e95d753c0bd477e7e36d0e683e3ec7b27f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 21 May 2013 16:18:15 -0400 Subject: Fix incremental bug in symmetry breaker. Thanks to Christoph Sticksel for reporting this. --- src/theory/uf/symmetry_breaker.cpp | 37 ++- src/theory/uf/symmetry_breaker.h | 28 +- src/theory/uf/theory_uf.cpp | 3 +- test/regress/regress0/GEO123+1.minimized.smt2 | 397 ++++++++++++++++++++++++++ test/regress/regress0/Makefile.am | 1 + 5 files changed, 462 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/GEO123+1.minimized.smt2 (limited to 'src/theory') diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index fcb6c3cd5..f5d7f9235 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -52,6 +52,8 @@ namespace CVC4 { namespace theory { namespace uf { +using namespace ::CVC4::context; + SymmetryBreaker::Template::Template() : d_template(), d_sets(), @@ -165,7 +167,10 @@ void SymmetryBreaker::Template::reset() { d_reps.clear(); } -SymmetryBreaker::SymmetryBreaker() : +SymmetryBreaker::SymmetryBreaker(context::Context* context) : + ContextNotifyObj(context), + d_assertionsToRerun(context), + d_rerunningAssertions(false), d_phi(), d_phiSet(), d_permutations(), @@ -175,6 +180,31 @@ SymmetryBreaker::SymmetryBreaker() : d_termEqs() { } +class SBGuard { + bool& d_ref; + bool d_old; +public: + SBGuard(bool& b) : d_ref(b), d_old(b) {} + ~SBGuard() { Debug("uf") << "reset to " << d_old << std::endl; d_ref = d_old; } +};/* class SBGuard */ + +void SymmetryBreaker::rerunAssertionsIfNecessary() { + if(d_rerunningAssertions || !d_phi.empty() || d_assertionsToRerun.empty()) { + return; + } + + SBGuard g(d_rerunningAssertions); + d_rerunningAssertions = true; + + Debug("ufsymm") << "UFSYMM: rerunning assertions..." << std::endl; + for(CDList::const_iterator i = d_assertionsToRerun.begin(); + i != d_assertionsToRerun.end(); + ++i) { + assertFormula(*i); + } + Debug("ufsymm") << "UFSYMM: DONE rerunning assertions..." << std::endl; +} + Node SymmetryBreaker::norm(TNode phi) { Node n = Rewriter::rewrite(phi); return normInternal(n); @@ -254,6 +284,10 @@ Node SymmetryBreaker::normInternal(TNode n) { } void SymmetryBreaker::assertFormula(TNode phi) { + rerunAssertionsIfNecessary(); + if(!d_rerunningAssertions) { + d_assertionsToRerun.push_back(phi); + } // use d_phi, put into d_permutations Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl; d_phi.push_back(phi); @@ -322,6 +356,7 @@ void SymmetryBreaker::clear() { } void SymmetryBreaker::apply(std::vector& newClauses) { + rerunAssertionsIfNecessary(); guessPermutations(); Debug("ufsymm") << "UFSYMM =====================================================" << endl << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index cf54b62c2..d04da048a 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -50,13 +50,15 @@ #include "expr/node.h" #include "expr/node_builder.h" +#include "context/context.h" +#include "context/cdlist.h" #include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace uf { -class SymmetryBreaker { +class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; @@ -92,6 +94,19 @@ public: private: + /** + * This class wasn't initially built to be incremental. It should + * be attached to a UserContext so that it clears everything when + * a pop occurs. This "assertionsToRerun" is a set of assertions to + * feed back through assertFormula() when we started getting things + * again. It's not just a matter of effectiveness, but also soundness; + * if some assertions (still in scope) are not seen by a symmetry-breaking + * round, then some symmetries that don't actually exist might be broken, + * leading to unsound results! + */ + context::CDList d_assertionsToRerun; + bool d_rerunningAssertions; + std::vector d_phi; std::set d_phiSet; Permutations d_permutations; @@ -101,6 +116,7 @@ private: TermEqs d_termEqs; void clear(); + void rerunAssertionsIfNecessary(); void guessPermutations(); bool invariantByPermutations(const Permutation& p); @@ -140,9 +156,17 @@ private: d_initNormalizationTimer, "theory::uf::symmetry_breaker::timers::initNormalization"); +protected: + + void contextNotifyPop() { + Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl; + clear(); + } + public: - SymmetryBreaker(); + SymmetryBreaker(context::Context* context); + ~SymmetryBreaker() throw() {} void assertFormula(TNode phi); void apply(std::vector& newClauses); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 69a963360..41935984f 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -38,7 +38,8 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_functionsTerms(c) + d_functionsTerms(c), + d_symb(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); diff --git a/test/regress/regress0/GEO123+1.minimized.smt2 b/test/regress/regress0/GEO123+1.minimized.smt2 new file mode 100644 index 000000000..8cc1fa7fd --- /dev/null +++ b/test/regress/regress0/GEO123+1.minimized.smt2 @@ -0,0 +1,397 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXIT: 10 +; +; This is a benchmark demonstrating a nasty incremental bug in the UF +; symmetry breaker, now fixed. +; +(set-logic QF_UF) +(declare-fun _substvar_29615_ () Bool) +(declare-sort T 0) +(declare-fun incident_o (T T) Bool) +(declare-fun sK25 () T) +(declare-fun sK26 () T) +(declare-fun ordered_by (T T T) Bool) +(declare-fun sK21 (T T) T) +(declare-fun incident_c (T T) Bool) +(declare-fun between_o (T T T T) Bool) +(declare-fun start_point (T T) Bool) +(declare-fun sK12 (T T) T) +(declare-fun meet (T T T) Bool) +(declare-fun end_point (T T) Bool) +(declare-fun inner_point (T T) Bool) +(declare-fun part_of (T T) Bool) +(declare-fun open (T) Bool) +(declare-fun sK22 (T T) T) +(declare-fun sK19 (T) T) +(declare-fun sum (T T) T) +(declare-fun sK4 (T T T) T) +(declare-fun sK2 (T T) T) +(declare-fun sK3 (T T) T) +(declare-fun sK0 (T T) T) +(declare-fun sK1 (T T T) T) +(declare-fun sK24 () T) +(declare-fun iProver_c13 () T) +(declare-fun iProver_c41 () T) +(declare-fun iProver_c14 () T) +(assert (incident_o sK26 sK24)) +(assert (not (ordered_by sK24 sK25 sK26))) +(assert (not (= sK25 sK26))) +(assert (start_point (sK19 sK24) sK24)) +(check-sat) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK24 sK25))) (or (= sK25 sK24) (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24))))) +(assert (let ((_let_0 (sK12 iProver_c13 sK25))) (or (= sK25 iProver_c13) (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK0 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK25 sK24)) (end_point _let_0 sK25)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK25 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK25 sK24)) (end_point _let_0 sK24)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK25 iProver_c13)) (end_point _let_0 iProver_c13)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (incident_c (sK4 sK24 sK25 _let_0) sK25) (meet _let_0 sK25 sK24)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (incident_c (sK4 iProver_c13 sK25 _let_0) sK25) (meet _let_0 sK25 iProver_c13)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (meet _let_0 sK25 sK24) (incident_c (sK4 sK24 sK25 _let_0) sK24)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c13)) (meet _let_0 sK25 iProver_c13) (incident_c (sK4 iProver_c13 sK25 _let_0) iProver_c13)))) +(assert (let ((_let_0 (sK4 sK24 sK25 (sK12 sK26 sK25)))) (or (not (incident_c (sK12 sK26 sK25) sK25)) (not (incident_c (sK12 sK26 sK25) sK24)) (meet (sK12 sK26 sK25) sK25 sK24) (not (end_point _let_0 sK25)) (not (end_point _let_0 sK24))))) +(assert (let ((_let_0 (sK4 iProver_c13 sK25 (sK12 sK26 sK25)))) (or (not (incident_c (sK12 sK26 sK25) sK25)) (not (incident_c (sK12 sK26 sK25) iProver_c13)) (meet (sK12 sK26 sK25) sK25 iProver_c13) (not (end_point _let_0 sK25)) (not (end_point _let_0 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (inner_point _let_0 sK25)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (part_of sK25 sK24))) (or (not (part_of sK24 sK24)) (not (incident_c _let_0 sK25)) _let_1 (not _let_1) (part_of sK24 sK25) (not (incident_c _let_0 sK24)) (not (end_point _let_0 sK24)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (part_of iProver_c13 iProver_c14)) (not (incident_c _let_0 sK25)) (part_of sK25 iProver_c13) (part_of iProver_c13 sK25) (not (incident_c _let_0 iProver_c13)) (not (part_of sK25 iProver_c14)) (not (end_point _let_0 iProver_c14))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (part_of (sK2 sK25 _let_0) sK25)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (part_of (sK3 sK25 _let_0) sK25)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (incident_c _let_0 (sK2 sK25 _let_0))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (incident_c _let_0 (sK3 sK25 _let_0))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (part_of (sK2 sK25 _let_0) (sK3 sK25 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (end_point _let_0 sK25) (not (part_of (sK3 sK25 _let_0) (sK2 sK25 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK25 sK24))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK25 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum sK24 sK25))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (incident_c _let_0 (sum iProver_c13 sK25))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK0 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK0 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK12 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK12 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK12 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK0 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (part_of sK25 sK24)) (incident_c _let_0 sK24)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (not (incident_c _let_0 sK25)) (not (part_of sK25 iProver_c13)) (incident_c _let_0 iProver_c13)))) +(assert (or (part_of sK24 sK25) (not (incident_c (sK0 sK24 sK25) sK25)))) +(assert (or (part_of iProver_c13 sK25) (not (incident_c (sK0 iProver_c13 sK25) sK25)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK12 sK24 sK26))) (or (= sK26 sK24) (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24))))) +(assert (let ((_let_0 (sK12 iProver_c13 sK26))) (or (= sK26 iProver_c13) (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK0 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK26 sK24)) (end_point _let_0 sK26)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK26 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (not (meet sK24 sK26 sK24)) (end_point _let_0 sK24)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (not (meet iProver_c14 sK26 iProver_c13)) (end_point _let_0 iProver_c13)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (incident_c (sK4 sK24 sK26 _let_0) sK26) (meet _let_0 sK26 sK24)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (incident_c (sK4 iProver_c13 sK26 _let_0) sK26) (meet _let_0 sK26 iProver_c13)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (meet _let_0 sK26 sK24) (incident_c (sK4 sK24 sK26 _let_0) sK24)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c13)) (meet _let_0 sK26 iProver_c13) (incident_c (sK4 iProver_c13 sK26 _let_0) iProver_c13)))) +(assert (let ((_let_0 (sK4 sK24 sK26 (sK12 sK25 sK26)))) (or (not (incident_c (sK12 sK25 sK26) sK26)) (not (incident_c (sK12 sK25 sK26) sK24)) (meet (sK12 sK25 sK26) sK26 sK24) (not (end_point _let_0 sK26)) (not (end_point _let_0 sK24))))) +(assert (let ((_let_0 (sK4 iProver_c13 sK26 (sK12 sK25 sK26)))) (or (not (incident_c (sK12 sK25 sK26) sK26)) (not (incident_c (sK12 sK25 sK26) iProver_c13)) (meet (sK12 sK25 sK26) sK26 iProver_c13) (not (end_point _let_0 sK26)) (not (end_point _let_0 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (inner_point _let_0 sK26)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (part_of sK26 sK24))) (or (not (part_of sK24 sK24)) (not (incident_c _let_0 sK26)) (part_of sK24 sK26) _let_1 (not _let_1) (not (incident_c _let_0 sK24)) (not (end_point _let_0 sK24)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (part_of iProver_c13 iProver_c14)) (not (incident_c _let_0 sK26)) (part_of iProver_c13 sK26) (part_of sK26 iProver_c13) (not (incident_c _let_0 iProver_c13)) (not (part_of sK26 iProver_c14)) (not (end_point _let_0 iProver_c14))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (part_of (sK2 sK26 _let_0) sK26)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (part_of (sK3 sK26 _let_0) sK26)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (incident_c _let_0 (sK2 sK26 _let_0))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (incident_c _let_0 (sK3 sK26 _let_0))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (part_of (sK2 sK26 _let_0) (sK3 sK26 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (end_point _let_0 sK26) (not (part_of (sK3 sK26 _let_0) (sK2 sK26 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK26 sK24))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK26 iProver_c13))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum sK24 sK26))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (incident_c _let_0 (sum iProver_c13 sK26))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK0 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK0 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK12 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK12 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK12 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK0 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (part_of sK26 sK24)) (incident_c _let_0 sK24)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (not (incident_c _let_0 sK26)) (not (part_of sK26 iProver_c13)) (incident_c _let_0 iProver_c13)))) +(assert (or (part_of sK24 sK26) (not (incident_c (sK0 sK24 sK26) sK26)))) +(assert (or (part_of iProver_c13 sK26) (not (incident_c (sK0 iProver_c13 sK26) sK26)))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK21 sK24 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK24 _let_0 _let_1)) (= sK25 sK24))))) +(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by iProver_c13 _let_0 _let_1)) (= sK25 iProver_c13))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 (sK22 sK26 sK25))) (incident_o _let_0 sK25)))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (or (not (ordered_by sK25 (sK21 sK26 sK25) _let_0)) (incident_o _let_0 sK25)))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 sK24)) (between_o sK25 _let_0 _let_1 sK24))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 iProver_c13)) (between_o sK25 _let_0 _let_1 iProver_c13))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 sK24)) (between_o sK25 sK24 _let_1 _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (or (not (ordered_by sK25 _let_0 _let_1)) (not (ordered_by sK25 _let_1 iProver_c13)) (between_o sK25 iProver_c13 _let_1 _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK21 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK22 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK24 sK25))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 iProver_c41 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c14 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1)))))) +(assert (let ((_let_0 (sK22 iProver_c14 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 _let_0 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 _let_0) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 _let_0 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 _let_0) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (or (incident_c (sK1 _let_0 _let_0 _let_0) _let_0) (= (sum _let_0 _let_0) _let_0)))) +(assert (let ((_let_0 (sK22 iProver_c13 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c13 sK25))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 sK24 sK25))) (let ((_let_2 (sK1 _let_0 sK24 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (incident_c _let_2 _let_0) (= (sum sK24 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK22 iProver_c14 sK25))) (let ((_let_2 (sK1 _let_0 iProver_c13 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (incident_c _let_2 _let_0) (= (sum iProver_c13 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (let ((_let_2 (sK1 sK24 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (= (sum _let_1 sK24) _let_0)))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (let ((_let_1 (sK22 sK26 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (= (sum _let_1 iProver_c13) _let_0)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 sK24 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum _let_0 sK24) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK1 iProver_c13 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum _let_0 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 sK24 sK25))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 iProver_c14 sK25))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1)))))) +(assert (let ((_let_0 (sK21 iProver_c14 sK25))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_1 _let_0))) (let ((_let_3 (sK22 _let_1 _let_0))) (or (ordered_by _let_0 _let_2 _let_3) (ordered_by _let_1 _let_2 _let_3) (= _let_0 _let_1))))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK21 _let_0 _let_1))) (let ((_let_3 (sK22 _let_0 _let_1))) (or (ordered_by _let_1 _let_2 _let_3) (ordered_by _let_0 _let_2 _let_3) (= _let_1 _let_0))))))) +(assert (let ((_let_0 (sK21 sK24 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK24 _let_0 _let_1)) (= sK26 sK24))))) +(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by iProver_c13 _let_0 _let_1)) (= sK26 iProver_c13))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 (sK22 sK25 sK26))) (incident_o _let_0 sK26)))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (or (not (ordered_by sK26 (sK21 sK25 sK26) _let_0)) (incident_o _let_0 sK26)))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 sK24)) (between_o sK26 _let_0 _let_1 sK24))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 iProver_c13)) (between_o sK26 _let_0 _let_1 iProver_c13))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 sK24)) (between_o sK26 sK24 _let_1 _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (or (not (ordered_by sK26 _let_0 _let_1)) (not (ordered_by sK26 _let_1 iProver_c13)) (between_o sK26 iProver_c13 _let_1 _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_1 _let_0))) (or (= _let_0 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK12 _let_0 _let_1))) (or (= _let_1 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 _let_0)))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK21 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (= _let_0 _let_1) (not (part_of _let_1 _let_0)) (open _let_1))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (or (= _let_1 _let_0) (not (part_of _let_0 _let_1)) (open _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (or (= _let_1 _let_0) (open _let_0) (not (part_of _let_0 _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK22 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK24 sK26))) (let ((_let_1 (sK1 sK24 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 sK24) _let_0))))) +(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK21 iProver_c41 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c14 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1)))))) +(assert (let ((_let_0 (sK22 iProver_c14 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 _let_0 sK24 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum sK24 _let_0) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 _let_0 iProver_c13 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum iProver_c13 _let_0) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (or (incident_c (sK1 _let_0 _let_0 _let_0) _let_0) (= (sum _let_0 _let_0) _let_0)))) +(assert (let ((_let_0 (sK22 iProver_c13 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c13 sK26))) (let ((_let_2 (sK1 _let_0 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (= (sum _let_0 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 sK24 sK26))) (let ((_let_2 (sK1 _let_0 sK24 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (incident_c _let_2 _let_0) (= (sum sK24 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK22 iProver_c14 sK26))) (let ((_let_2 (sK1 _let_0 iProver_c13 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (incident_c _let_2 _let_0) (= (sum iProver_c13 _let_0) _let_1)))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (let ((_let_2 (sK1 sK24 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 sK24) (= (sum _let_1 sK24) _let_0)))))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (let ((_let_1 (sK22 sK25 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_1 _let_0))) (or (incident_c _let_2 _let_0) (incident_c _let_2 _let_1) (incident_c _let_2 iProver_c13) (= (sum _let_1 iProver_c13) _let_0)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 sK24 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 sK24) (= (sum _let_0 sK24) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK1 iProver_c13 _let_0 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c13) (= (sum _let_0 iProver_c13) _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 sK24 sK26))) (let ((_let_2 (sK1 sK24 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 sK24) (= (sum _let_0 sK24) _let_1)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 iProver_c14 sK26))) (let ((_let_2 (sK1 iProver_c13 _let_0 _let_1))) (or (incident_c _let_2 _let_1) (incident_c _let_2 _let_0) (incident_c _let_2 iProver_c13) (= (sum _let_0 iProver_c13) _let_1)))))) +(assert (let ((_let_0 (sK21 iProver_c14 sK26))) (let ((_let_1 (sK1 iProver_c13 iProver_c14 _let_0))) (or (incident_c _let_1 _let_0) (incident_c _let_1 iProver_c14) (incident_c _let_1 iProver_c13) (= (sum iProver_c14 iProver_c13) _let_0))))) +(assert (or (= iProver_c13 iProver_c14) false false _substvar_29615_ false false)) +(assert (or (not (incident_c sK24 sK24)) (not (meet sK24 sK25 sK24)) (not (incident_c sK24 sK25)) (end_point sK24 sK25))) +(assert (or (not (meet iProver_c14 sK25 iProver_c13)) (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (incident_c sK24 iProver_c13)))) +(assert (or (not (incident_c sK24 sK24)) (end_point sK24 sK24) (not (meet sK24 sK25 sK24)) (not (incident_c sK24 sK25)))) +(assert (or (not (meet iProver_c14 sK25 iProver_c13)) (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (end_point sK24 iProver_c13))) +(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (incident_c (sK4 sK24 sK25 sK24) sK25))) +(assert (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (incident_c (sK4 iProver_c13 sK25 sK24) sK25) (meet sK24 sK25 iProver_c13))) +(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (incident_c (sK4 sK24 sK25 sK24) sK24))) +(assert (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (meet sK24 sK25 iProver_c13) (incident_c (sK4 iProver_c13 sK25 sK24) iProver_c13))) +(assert (let ((_let_0 (sK4 sK24 sK25 sK24))) (or (not (incident_c sK24 sK24)) (meet sK24 sK25 sK24) (not (incident_c sK24 sK25)) (not (end_point _let_0 sK25)) (not (end_point _let_0 sK24))))) +(assert (let ((_let_0 (sK4 iProver_c13 sK25 sK24))) (or (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (meet sK24 sK25 iProver_c13) (not (end_point _let_0 sK25)) (not (end_point _let_0 iProver_c13))))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (inner_point sK24 sK25))) +(assert (let ((_let_0 (part_of sK25 sK24))) (or (not (incident_c sK24 sK24)) (not (part_of sK24 sK24)) (not (end_point sK24 sK24)) _let_0 (not _let_0) (part_of sK24 sK25) (not (incident_c sK24 sK25))))) +(assert (or (not (part_of iProver_c13 iProver_c14)) (part_of sK25 iProver_c13) (part_of iProver_c13 sK25) (not (part_of sK25 iProver_c14)) (not (incident_c sK24 sK25)) (not (incident_c sK24 iProver_c13)) (not (end_point sK24 iProver_c14)))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (part_of (sK2 sK25 sK24) sK25))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (part_of (sK3 sK25 sK24) sK25))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (incident_c sK24 (sK2 sK25 sK24)))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (incident_c sK24 (sK3 sK25 sK24)))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (part_of (sK2 sK25 sK24) (sK3 sK25 sK24))))) +(assert (or (not (incident_c sK24 sK25)) (end_point sK24 sK25) (not (part_of (sK3 sK25 sK24) (sK2 sK25 sK24))))) +(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK25 sK24)))) +(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK25 iProver_c13)))) +(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum sK24 sK25)))) +(assert (or (not (incident_c sK24 sK25)) (incident_c sK24 (sum iProver_c13 sK25)))) +(assert (or (incident_c sK24 sK24) (not (part_of sK25 sK24)) (not (incident_c sK24 sK25)))) +(assert (or (not (part_of sK25 iProver_c13)) (not (incident_c sK24 sK25)) (incident_c sK24 iProver_c13))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24)))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2)))))) +(assert (let ((_let_0 (sK12 sK26 sK25))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (or (not (incident_c sK24 sK24)) (not (meet sK24 sK26 sK24)) (not (incident_c sK24 sK26)) (end_point sK24 sK26))) +(assert (or (not (meet iProver_c14 sK26 iProver_c13)) (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (end_point sK24 sK26))) +(assert (or (not (incident_c sK24 sK24)) (end_point sK24 sK24) (not (meet sK24 sK26 sK24)) (not (incident_c sK24 sK26)))) +(assert (or (not (meet iProver_c14 sK26 iProver_c13)) (not (incident_c sK24 iProver_c13)) (end_point sK24 iProver_c13) (not (incident_c sK24 sK26)))) +(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (incident_c (sK4 sK24 sK26 sK24) sK26))) +(assert (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (incident_c (sK4 iProver_c13 sK26 sK24) sK26) (meet sK24 sK26 iProver_c13))) +(assert (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (incident_c (sK4 sK24 sK26 sK24) sK24))) +(assert (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (meet sK24 sK26 iProver_c13) (incident_c (sK4 iProver_c13 sK26 sK24) iProver_c13))) +(assert (let ((_let_0 (sK4 sK24 sK26 sK24))) (or (not (incident_c sK24 sK24)) (meet sK24 sK26 sK24) (not (incident_c sK24 sK26)) (not (end_point _let_0 sK26)) (not (end_point _let_0 sK24))))) +(assert (let ((_let_0 (sK4 iProver_c13 sK26 sK24))) (or (not (incident_c sK24 iProver_c13)) (not (incident_c sK24 sK26)) (meet sK24 sK26 iProver_c13) (not (end_point _let_0 sK26)) (not (end_point _let_0 iProver_c13))))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (inner_point sK24 sK26))) +(assert (let ((_let_0 (part_of sK26 sK24))) (or (not (incident_c sK24 sK24)) (not (part_of sK24 sK24)) (not (end_point sK24 sK24)) (part_of sK24 sK26) _let_0 (not _let_0) (not (incident_c sK24 sK26))))) +(assert (or (not (part_of iProver_c13 iProver_c14)) (part_of iProver_c13 sK26) (part_of sK26 iProver_c13) (not (part_of sK26 iProver_c14)) (not (incident_c sK24 iProver_c13)) (not (end_point sK24 iProver_c14)) (not (incident_c sK24 sK26)))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (part_of (sK2 sK26 sK24) sK26))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (part_of (sK3 sK26 sK24) sK26))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (incident_c sK24 (sK2 sK26 sK24)))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (incident_c sK24 (sK3 sK26 sK24)))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (not (part_of (sK2 sK26 sK24) (sK3 sK26 sK24))))) +(assert (or (not (incident_c sK24 sK26)) (end_point sK24 sK26) (not (part_of (sK3 sK26 sK24) (sK2 sK26 sK24))))) +(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK26 sK24)))) +(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK26 iProver_c13)))) +(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum sK24 sK26)))) +(assert (or (not (incident_c sK24 sK26)) (incident_c sK24 (sum iProver_c13 sK26)))) +(assert (or (incident_c sK24 sK24) (not (part_of sK26 sK24)) (not (incident_c sK24 sK26)))) +(assert (or (not (part_of sK26 iProver_c13)) (incident_c sK24 iProver_c13) (not (incident_c sK24 sK26)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24)))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2)))))) +(assert (let ((_let_0 (sK12 sK25 sK26))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (let ((_let_0 (sK1 sK24 sK24 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 sK24)) (= (sum sK24 sK24) sK25)))) +(assert (let ((_let_0 (sK1 iProver_c13 iProver_c14 sK25))) (or (not (incident_c _let_0 sK25)) (not (incident_c _let_0 iProver_c14)) (= (sum iProver_c14 iProver_c13) sK25)))) +(assert (let ((_let_0 (sK1 sK24 sK24 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 sK24)) (= (sum sK24 sK24) sK26)))) +(assert (let ((_let_0 (sK1 iProver_c13 iProver_c14 sK26))) (or (not (incident_c _let_0 sK26)) (not (incident_c _let_0 iProver_c14)) (= (sum iProver_c14 iProver_c13) sK26)))) +(assert (let ((_let_0 (sum sK24 sK24))) (or (open sK25) (= _let_0 sK25) (not (part_of sK25 _let_0))))) +(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open sK25) (= _let_0 sK25) (not (part_of sK25 _let_0))))) +(assert (let ((_let_0 (sum sK24 sK24))) (or (open sK26) (= _let_0 sK26) (not (part_of sK26 _let_0))))) +(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open sK26) (= _let_0 sK26) (not (part_of sK26 _let_0))))) +(assert (let ((_let_0 (sum sK24 sK24))) (or (open _let_0) (not (part_of _let_0 sK25)) (= sK25 _let_0)))) +(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open _let_0) (not (part_of _let_0 sK25)) (= sK25 _let_0)))) +(assert (let ((_let_0 (sum sK24 sK24))) (or (open _let_0) (not (part_of _let_0 sK26)) (= sK26 _let_0)))) +(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (or (open _let_0) (not (part_of _let_0 sK26)) (= sK26 _let_0)))) +(assert (let ((_let_0 (sum sK24 sK24))) (let ((_let_1 (sK12 _let_0 sK25))) (or (= sK25 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK25))))) +(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (let ((_let_1 (sK12 _let_0 sK25))) (or (= sK25 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK25))))) +(assert (let ((_let_0 (sum sK24 sK24))) (let ((_let_1 (sK12 _let_0 sK26))) (or (= sK26 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK26))))) +(assert (let ((_let_0 (sum iProver_c13 iProver_c14))) (let ((_let_1 (sK12 _let_0 sK26))) (or (= sK26 _let_0) (incident_c _let_1 _let_0) (incident_c _let_1 sK26))))) +(assert (let ((_let_0 (sK19 sK24))) (or (not (incident_o sK25 sK24)) (not (start_point _let_0 sK24)) (ordered_by sK24 _let_0 sK25) (= _let_0 sK25)))) +(assert (let ((_let_0 (sK19 iProver_c13))) (or (not (start_point _let_0 iProver_c13)) (not (incident_o sK25 iProver_c13)) (ordered_by iProver_c13 _let_0 sK25) (= _let_0 sK25)))) +(assert (let ((_let_0 (sK19 sK24))) (or (not (incident_o sK26 sK24)) (not (start_point _let_0 sK24)) (ordered_by sK24 _let_0 sK26) (= _let_0 sK26)))) +(assert (let ((_let_0 (sK19 iProver_c13))) (or (not (start_point _let_0 iProver_c13)) (not (incident_o sK26 iProver_c13)) (ordered_by iProver_c13 _let_0 sK26) (= _let_0 sK26)))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (or (incident_o _let_0 sK26) (not (ordered_by sK26 _let_0 sK24))))) +(assert (or (not (ordered_by sK26 (sK21 sK25 sK26) sK24)) (incident_o sK24 sK26))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 sK24)) (between_o sK26 _let_0 sK24 sK24)))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 iProver_c13)) (between_o sK26 _let_0 sK24 iProver_c13)))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 sK24)) (between_o sK26 sK24 sK24 _let_0)))) +(assert (let ((_let_0 (sK21 sK25 sK26))) (or (not (ordered_by sK26 _let_0 sK24)) (not (ordered_by sK26 sK24 iProver_c13)) (between_o sK26 iProver_c13 sK24 _let_0)))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24)))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2)))))) +(assert (let ((_let_0 (sK22 sK25 sK26))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (or (incident_o _let_0 sK25) (not (ordered_by sK25 _let_0 sK24))))) +(assert (or (not (ordered_by sK25 (sK21 sK26 sK25) sK24)) (incident_o sK24 sK25))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 sK24)) (between_o sK25 _let_0 sK24 sK24)))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 iProver_c13)) (between_o sK25 _let_0 sK24 iProver_c13)))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 sK24)) (between_o sK25 sK24 sK24 _let_0)))) +(assert (let ((_let_0 (sK21 sK26 sK25))) (or (not (ordered_by sK25 _let_0 sK24)) (not (ordered_by sK25 sK24 iProver_c13)) (between_o sK25 iProver_c13 sK24 _let_0)))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 _let_0 sK24))) (let ((_let_2 (sK22 _let_0 sK24))) (or (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2) (= sK24 _let_0)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK12 _let_0 sK24))) (or (= sK24 _let_0) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (or (open _let_0) (= sK24 _let_0) (not (part_of _let_0 sK24))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (or (open sK24) (not (part_of sK24 _let_0)) (= _let_0 sK24)))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK21 sK24 _let_0))) (let ((_let_2 (sK22 sK24 _let_0))) (or (= _let_0 sK24) (ordered_by sK24 _let_1 _let_2) (ordered_by _let_0 _let_1 _let_2)))))) +(assert (let ((_let_0 (sK22 sK26 sK25))) (let ((_let_1 (sK12 sK24 _let_0))) (or (= _let_0 sK24) (incident_c _let_1 sK24) (incident_c _let_1 _let_0))))) +(check-sat) + diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index fec081ca8..4c14de996 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -115,6 +115,7 @@ TPTP_TESTS = \ # Regression tests derived from bug reports BUG_TESTS = \ + GEO123+1.minimized.smt2 \ smt2output.smt2 \ bug32.cvc \ bug49.smt \ -- cgit v1.2.3 From 7709fff002e3345bd727eaef2677e28830efb84d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 21 May 2013 18:39:33 -0400 Subject: Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to improper ITE removal in quantifier instantiations. --- src/theory/theory_engine.cpp | 12 ++++++++++++ src/util/ite_removal.cpp | 6 +++++- test/regress/regress0/Makefile.am | 3 ++- test/regress/regress0/bug512.minimized.smt2 | 8 ++++++++ 4 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/bug512.minimized.smt2 (limited to 'src/theory') diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ee37f331e..53f5d10f3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1311,6 +1311,18 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable d_iteRemover.run(additionalLemmas, iteSkolemMap); additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + if(Trace.isOn("lemma-ites")) { + Debug("lemma-ites") << "removed ITEs from lemma: " << node << std::endl; + Debug("lemma-ites") << " + now have the following " + << additionalLemmas.size() << " lemma(s):" << std::endl; + for(std::vector::const_iterator i = additionalLemmas.begin(); + i != additionalLemmas.end(); + ++i) { + Debug("lemma-ites") << " + " << *i << std::endl; + } + Debug("lemma-ites") << std::endl; + } + // assert to prop engine d_propEngine->assertLemma(additionalLemmas[0], negated, removable); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index f26bbe0aa..7d4948251 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -30,7 +30,11 @@ void RemoveITE::run(std::vector& output, IteSkolemMap& iteSkolemMap) { for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { std::vector quantVar; - output[i] = run(output[i], output, iteSkolemMap, quantVar); + // Do this in two steps to avoid Node problems(?) + // Appears related to bug 512, splitting this into two lines + // fixes the bug on clang on Mac OS + Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar); + output[i] = itesRemoved; } } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 4c14de996..6cdd18403 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -151,7 +151,8 @@ BUG_TESTS = \ bug484.smt2 \ bug486.cvc \ bug497.cvc \ - bug507.smt2 + bug507.smt2 \ + bug512.minimized.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug512.minimized.smt2 b/test/regress/regress0/bug512.minimized.smt2 new file mode 100644 index 000000000..5fcbf5a9f --- /dev/null +++ b/test/regress/regress0/bug512.minimized.smt2 @@ -0,0 +1,8 @@ +; EXPECT: unknown +; EXIT: 0 +(set-logic UF) +(declare-sort T 0) +(declare-fun bool_2_U (Bool) T) +(declare-fun U_2_bool (T) Bool) +(assert (forall ((x T)) (= (bool_2_U (U_2_bool x)) x))) +(check-sat) -- cgit v1.2.3 From 852d41b2878ae4981ab4a9b246345bb05bbe23ab Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 May 2013 16:33:15 -0500 Subject: Add regressions for finite model finding --- src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/quantifiers_engine.cpp | 5 +- test/regress/regress0/Makefile.am | 4 +- test/regress/regress0/fmf/ALG008-1.smt2 | 73 ++++ .../regress0/fmf/Arrow_Order-smtlib.778341.smt | 265 ++++++++++++ test/regress/regress0/fmf/Hoare-z3.931718.smt | 50 +++ test/regress/regress0/fmf/Makefile.am | 47 ++ test/regress/regress0/fmf/PUZ001+1.smt2 | 119 ++++++ test/regress/regress0/fmf/QEpres-uf.855035.smt | 85 ++++ test/regress/regress0/fmf/agree466.smt2 | 475 +++++++++++++++++++++ test/regress/regress0/fmf/agree467.smt2 | 342 +++++++++++++++ test/regress/regress0/fmf/german169.smt2 | 104 +++++ test/regress/regress0/fmf/german73.smt2 | 106 +++++ test/regress/regress0/fmf/refcount24.cvc.smt2 | 38 ++ 14 files changed, 1710 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress0/fmf/ALG008-1.smt2 create mode 100644 test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt create mode 100644 test/regress/regress0/fmf/Hoare-z3.931718.smt create mode 100755 test/regress/regress0/fmf/Makefile.am create mode 100644 test/regress/regress0/fmf/PUZ001+1.smt2 create mode 100644 test/regress/regress0/fmf/QEpres-uf.855035.smt create mode 100644 test/regress/regress0/fmf/agree466.smt2 create mode 100644 test/regress/regress0/fmf/agree467.smt2 create mode 100755 test/regress/regress0/fmf/german169.smt2 create mode 100755 test/regress/regress0/fmf/german73.smt2 create mode 100755 test/regress/regress0/fmf/refcount24.cvc.smt2 (limited to 'src/theory') diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 060f6dbba..dd5e404c6 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1376,7 +1376,7 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){ Assert(!done()); TNode assertion = get(); - if( options::finiteModelFind() ){ + if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){ d_quantEngine->getBoundedIntegers()->assertNode(assertion); } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ef8169433..e01d83853 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -62,8 +62,9 @@ d_lemmas_produced_c(u){ d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); - d_bint = new quantifiers::BoundedIntegers( c, this ); - d_modules.push_back( d_bint ); + //d_bint = new quantifiers::BoundedIntegers( c, this ); + //d_modules.push_back( d_bint ); + d_bint = NULL; }else{ d_model_engine = NULL; d_bint = NULL; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 6cdd18403..c51b505bc 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision -DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf +DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf BINARY = cvc4 LOG_COMPILER = @srcdir@/../run_regression diff --git a/test/regress/regress0/fmf/ALG008-1.smt2 b/test/regress/regress0/fmf/ALG008-1.smt2 new file mode 100644 index 000000000..018006f45 --- /dev/null +++ b/test/regress/regress0/fmf/ALG008-1.smt2 @@ -0,0 +1,73 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +;%-------------------------------------------------------------------------- +;% File : ALG008-1 : TPTP v5.4.0. Released v2.2.0. +;% Domain : General Algebra +;% Problem : TC + right identity does not give RC. +;% Version : [MP96] (equality) axioms : Especial. +;% English : An algebra with a right identity satisfying the Thomsen +;% Closure (RC) condition does not necessarily satisfy the +;% Reidemeister Closure (RC) condition. + +;% Refs : [McC98] McCune (1998), Email to G. Sutcliffe +;% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq +;% Source : [McC98] +;% Names : TC-3 [MP96] + +;% Status : Satisfiable +;% Rating : 0.50 v5.4.0, 0.80 v5.3.0, 0.78 v5.2.0, 0.80 v5.0.0, 0.78 v4.1.0, 0.71 v4.0.1, 0.80 v4.0.0, 0.50 v3.7.0, 0.33 v3.4.0, 0.50 v3.3.0, 0.33 v3.2.0, 0.80 v3.1.0, 0.67 v2.7.0, 0.33 v2.6.0, 0.86 v2.5.0, 0.50 v2.4.0, 0.67 v2.3.0, 1.00 v2.2.1 +;% Syntax : Number of clauses : 6 ( 0 non-Horn; 5 unit; 5 RR) +;% Number of atoms : 10 ( 10 equality) +;% Maximal clause size : 5 ( 2 average) +;% Number of predicates : 1 ( 0 propositional; 2-2 arity) +;% Number of functors : 9 ( 8 constant; 0-2 arity) +;% Number of variables : 9 ( 0 singleton) +;% Maximal term depth : 2 ( 2 average) +;% SPC : CNF_SAT_RFO_EQU_NUE + +;% Comments : The smallest model has 3 elements. +;%-------------------------------------------------------------------------- +;%----Thomsen Closure (TC) condition: +(set-logic UF) +(set-info :status sat) +(declare-sort sort__smt2 0) +; functions +(declare-fun multiply__smt2_2 ( sort__smt2 sort__smt2 ) sort__smt2) +(declare-fun identity__smt2_0 ( ) sort__smt2) +(declare-fun c4__smt2_0 ( ) sort__smt2) +(declare-fun a__smt2_0 ( ) sort__smt2) +(declare-fun c3__smt2_0 ( ) sort__smt2) +(declare-fun b__smt2_0 ( ) sort__smt2) +(declare-fun c2__smt2_0 ( ) sort__smt2) +(declare-fun c1__smt2_0 ( ) sort__smt2) +(declare-fun f__smt2_0 ( ) sort__smt2) +; predicates + +; thomsen_closure axiom +(assert (forall ((?V7 sort__smt2) (?V6 sort__smt2) (?W sort__smt2) (?V sort__smt2) (?U sort__smt2) (?Z sort__smt2) (?Y sort__smt2) (?X sort__smt2)) + (or (not (= (multiply__smt2_2 ?X ?Y) ?Z)) + (not (= (multiply__smt2_2 ?U ?V) ?Z)) + (not (= (multiply__smt2_2 ?X ?W) ?V6)) + (not (= (multiply__smt2_2 ?V7 ?V) ?V6)) + (= (multiply__smt2_2 ?U ?W) (multiply__smt2_2 ?V7 ?Y)))) ) + +;%----Right identity: +; right_identity axiom +(assert (forall ((?X sort__smt2)) (= (multiply__smt2_2 ?X identity__smt2_0) ?X)) ) + +;%----Denial of Reidimeister Closure (RC) condidition. +; prove_reidimeister1 negated_conjecture +(assert (= (multiply__smt2_2 c4__smt2_0 a__smt2_0) (multiply__smt2_2 c3__smt2_0 b__smt2_0)) ) + +; prove_reidimeister2 negated_conjecture +(assert (= (multiply__smt2_2 c2__smt2_0 a__smt2_0) (multiply__smt2_2 c1__smt2_0 b__smt2_0)) ) + +; prove_reidimeister3 negated_conjecture +(assert (= (multiply__smt2_2 c4__smt2_0 f__smt2_0) (multiply__smt2_2 c3__smt2_0 identity__smt2_0)) ) + +; prove_reidimeister4 negated_conjecture +(assert (not (= (multiply__smt2_2 c2__smt2_0 f__smt2_0) (multiply__smt2_2 c1__smt2_0 identity__smt2_0))) ) + + +(check-sat) diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt new file mode 100644 index 000000000..644d29737 --- /dev/null +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -0,0 +1,265 @@ +% COMMAND-LINE: --finite-model-find +% EXPECT: unsat +% EXIT: 20 +(benchmark Isabelle +:status sat +:logic AUFLIA +:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18 S19 S20 S21 S22 S23 S24 S25 S26 S27 S28 S29 S30 S31 S32 S33 S34 S35 S36 S37) +:extrafuns ( + (f1 S1) + (f2 S1) + (f3 S3 S2 S1) + (f4 S4 S2 S3) + (f5 S4) + (f6 S6 S5 S1) + (f7 S7 S5 S6) + (f8 S7) + (f9 S9 S8 S1) + (f10 S10 S8 S9) + (f11 S10) + (f12 S1) + (f13 S12 S1) + (f14 S12) + (f15 S12 S1) + (f16 S2) + (f17 S13 S2 S2) + (f18 S14 S11 S13) + (f19 S14) + (f20 S5) + (f21 S16 S5 S5) + (f22 S17 S15 S16) + (f23 S17) + (f24 S8) + (f25 S18 S8 S8) + (f26 S19 S5 S18) + (f27 S19) + (f28 S20 S2 S13) + (f29 S20) + (f30 S21 S5 S16) + (f31 S21) + (f32 S22 S8 S18) + (f33 S22) + (f34 S14) + (f35 S17) + (f36 S19) + (f37 S24 S23 S2) + (f38 S25 S2 S24) + (f39 S25) + (f40 S26 S23 S1) + (f41 S27 Int S26) + (f42 S27) + (f43 S28 S23 S5) + (f44 S29 S5 S28) + (f45 S29) + (f46 S30 S23 S8) + (f47 S31 S8 S30) + (f48 S31) + (f49 S2 S1) + (f50 S5 S1) + (f51 S8 S1) + (f52 S4) + (f53 S7) + (f54 S10) + (f55 S32 S2 S11) + (f56 S32) + (f57 S33 S5 S15) + (f58 S33) + (f59 S34 S8 S5) + (f60 S34) + (f61 S35 S11 S1) + (f62 S2 S35) + (f63 S36 S15 S1) + (f64 S5 S36) + (f65 S8 S6) + (f66 S35 S3) + (f67 S36 S6) + (f68 S6 S9) + (f69 S11 S3) + (f70 S5 S9) + (f71 S15 S6) + (f72 S13) + (f73 S16) + (f74 S18) + (f75 S20) + (f76 S21) + (f77 S22) + (f78 S37 S26 Int) + (f79 S37) +) +:assumption (not (= f1 f2)) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f8 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f11 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (not (= f12 f1)) +:assumption (forall (?v0 S11) (?v1 S11) (implies (not (= ?v0 ?v1)) (= f12 f1))) +:assumption (exists (?v0 S11) (?v1 S11) (?v2 S11) (distinct ?v0 ?v1 ?v2)) +:assumption (exists (?v0 S11) (?v1 S11) (?v2 S11) (distinct ?v0 ?v1 ?v2) ) +:assumption (= (f13 f14) f1) +:assumption (= (f15 f14) f1) +:assumption (forall (?v0 S11) (?v1 S11) (implies (not (= ?v0 ?v1)) (exists (?v2 S11) (distinct ?v0 ?v1 ?v2))) ) +:assumption (forall (?v0 S11) (?v1 S2) (not (= f16 (f17 (f18 f19 ?v0) ?v1))) ) +:assumption (forall (?v0 S15) (?v1 S5) (not (= f20 (f21 (f22 f23 ?v0) ?v1))) ) +:assumption (forall (?v0 S5) (?v1 S8) (not (= f24 (f25 (f26 f27 ?v0) ?v1))) ) +:assumption (forall (?v0 S11) (?v1 S2) (not (= (f17 (f18 f19 ?v0) ?v1) f16)) ) +:assumption (forall (?v0 S15) (?v1 S5) (not (= (f21 (f22 f23 ?v0) ?v1) f20)) ) +:assumption (forall (?v0 S5) (?v1 S8) (not (= (f25 (f26 f27 ?v0) ?v1) f24)) ) +:assumption (forall (?v0 S2) (iff (not (= ?v0 f16)) (exists (?v1 S11) (?v2 S2) (= ?v0 (f17 (f18 f19 ?v1) ?v2)))) ) +:assumption (forall (?v0 S5) (iff (not (= ?v0 f20)) (exists (?v1 S15) (?v2 S5) (= ?v0 (f21 (f22 f23 ?v1) ?v2)))) ) +:assumption (forall (?v0 S8) (iff (not (= ?v0 f24)) (exists (?v1 S5) (?v2 S8) (= ?v0 (f25 (f26 f27 ?v1) ?v2)))) ) +:assumption (forall (?v0 S2) (implies (implies (= ?v0 f16) false) (implies (forall (?v1 S11) (?v2 S2) (implies (= ?v0 (f17 (f18 f19 ?v1) ?v2)) false)) false)) ) +:assumption (forall (?v0 S5) (implies (implies (= ?v0 f20) false) (implies (forall (?v1 S15) (?v2 S5) (implies (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false)) ) +:assumption (forall (?v0 S8) (implies (implies (= ?v0 f24) false) (implies (forall (?v1 S5) (?v2 S8) (implies (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false)) ) +:assumption (forall (?v0 S2) (?v1 S11) (not (= ?v0 (f17 (f18 f19 ?v1) ?v0))) ) +:assumption (forall (?v0 S8) (?v1 S5) (not (= ?v0 (f25 (f26 f27 ?v1) ?v0))) ) +:assumption (forall (?v0 S5) (?v1 S15) (not (= ?v0 (f21 (f22 f23 ?v1) ?v0))) ) +:assumption (forall (?v0 S11) (?v1 S2) (not (= (f17 (f18 f19 ?v0) ?v1) ?v1)) ) +:assumption (forall (?v0 S5) (?v1 S8) (not (= (f25 (f26 f27 ?v0) ?v1) ?v1)) ) +:assumption (forall (?v0 S15) (?v1 S5) (not (= (f21 (f22 f23 ?v0) ?v1) ?v1)) ) +:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2) (iff (= (f17 (f18 f19 ?v0) ?v1) (f17 (f18 f19 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ) +:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8) (iff (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ) +:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5) (iff (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ) +:assumption (forall (?v0 S11) (?v1 S2) (= (f17 (f28 f29 (f17 (f18 f19 ?v0) ?v1)) f16) (f17 (f18 f19 ?v0) ?v1)) ) +:assumption (forall (?v0 S15) (?v1 S5) (= (f21 (f30 f31 (f21 (f22 f23 ?v0) ?v1)) f20) (f21 (f22 f23 ?v0) ?v1)) ) +:assumption (forall (?v0 S5) (?v1 S8) (= (f25 (f32 f33 (f25 (f26 f27 ?v0) ?v1)) f24) (f25 (f26 f27 ?v0) ?v1)) ) +:assumption (forall (?v0 S11) (= (f17 (f18 f34 ?v0) f16) (f17 (f18 f19 ?v0) f16)) ) +:assumption (forall (?v0 S15) (= (f21 (f22 f35 ?v0) f20) (f21 (f22 f23 ?v0) f20)) ) +:assumption (forall (?v0 S5) (= (f25 (f26 f36 ?v0) f24) (f25 (f26 f27 ?v0) f24)) ) +:assumption (forall (?v0 S2) (?v1 S3) (implies (not (= ?v0 f16)) (implies (forall (?v2 S11) (= (f3 ?v1 (f17 (f18 f19 ?v2) f16)) f1)) (implies (forall (?v2 S11) (?v3 S2) (implies (not (= ?v3 f16)) (implies (= (f3 ?v1 ?v3) f1) (= (f3 ?v1 (f17 (f18 f19 ?v2) ?v3)) f1)))) (= (f3 ?v1 ?v0) f1)))) ) +:assumption (forall (?v0 S5) (?v1 S6) (implies (not (= ?v0 f20)) (implies (forall (?v2 S15) (= (f6 ?v1 (f21 (f22 f23 ?v2) f20)) f1)) (implies (forall (?v2 S15) (?v3 S5) (implies (not (= ?v3 f20)) (implies (= (f6 ?v1 ?v3) f1) (= (f6 ?v1 (f21 (f22 f23 ?v2) ?v3)) f1)))) (= (f6 ?v1 ?v0) f1)))) ) +:assumption (forall (?v0 S8) (?v1 S9) (implies (not (= ?v0 f24)) (implies (forall (?v2 S5) (= (f9 ?v1 (f25 (f26 f27 ?v2) f24)) f1)) (implies (forall (?v2 S5) (?v3 S8) (implies (not (= ?v3 f24)) (implies (= (f9 ?v1 ?v3) f1) (= (f9 ?v1 (f25 (f26 f27 ?v2) ?v3)) f1)))) (= (f9 ?v1 ?v0) f1)))) ) +:assumption (forall (?v0 S11) (?v1 S23) (= (f37 (f38 f39 (f17 (f18 f19 ?v0) f16)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f17 (f18 f19 ?v0) f16) f16)) ) +:assumption (forall (?v0 S15) (?v1 S23) (= (f43 (f44 f45 (f21 (f22 f23 ?v0) f20)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f21 (f22 f23 ?v0) f20) f20)) ) +:assumption (forall (?v0 S5) (?v1 S23) (= (f46 (f47 f48 (f25 (f26 f27 ?v0) f24)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f25 (f26 f27 ?v0) f24) f24)) ) +:assumption (forall (?v0 S23) (= (f37 (f38 f39 f16) ?v0) f16) ) +:assumption (forall (?v0 S23) (= (f43 (f44 f45 f20) ?v0) f20) ) +:assumption (forall (?v0 S23) (= (f46 (f47 f48 f24) ?v0) f24) ) +:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2) (= (f17 (f28 f29 (f17 (f18 f19 ?v0) ?v1)) (f17 (f18 f19 ?v2) ?v3)) (f17 (f18 f19 ?v0) (f17 (f18 f19 ?v2) (f17 (f28 f29 ?v1) ?v3)))) ) +:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8) (= (f25 (f32 f33 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f25 (f26 f27 ?v0) (f25 (f26 f27 ?v2) (f25 (f32 f33 ?v1) ?v3)))) ) +:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5) (= (f21 (f30 f31 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f21 (f22 f23 ?v0) (f21 (f22 f23 ?v2) (f21 (f30 f31 ?v1) ?v3)))) ) +:assumption (forall (?v0 S2) (= (f17 (f28 f29 ?v0) f16) ?v0) ) +:assumption (forall (?v0 S5) (= (f21 (f30 f31 ?v0) f20) ?v0) ) +:assumption (forall (?v0 S8) (= (f25 (f32 f33 ?v0) f24) ?v0) ) +:assumption (forall (?v0 S2) (= (f17 (f28 f29 f16) ?v0) ?v0) ) +:assumption (forall (?v0 S5) (= (f21 (f30 f31 f20) ?v0) ?v0) ) +:assumption (forall (?v0 S8) (= (f25 (f32 f33 f24) ?v0) ?v0) ) +:assumption (forall (?v0 S2) (iff (= ?v0 f16) (= (f49 ?v0) f1)) ) +:assumption (forall (?v0 S5) (iff (= ?v0 f20) (= (f50 ?v0) f1)) ) +:assumption (forall (?v0 S8) (iff (= ?v0 f24) (= (f51 ?v0) f1)) ) +:assumption (forall (?v0 S2) (iff (= (f49 ?v0) f1) (= ?v0 f16)) ) +:assumption (forall (?v0 S5) (iff (= (f50 ?v0) f1) (= ?v0 f20)) ) +:assumption (forall (?v0 S8) (iff (= (f51 ?v0) f1) (= ?v0 f24)) ) +:assumption (iff (= (f49 f16) f1) true) +:assumption (iff (= (f50 f20) f1) true) +:assumption (iff (= (f51 f24) f1) true) +:assumption (forall (?v0 S11) (?v1 S2) (iff (= (f49 (f17 (f18 f19 ?v0) ?v1)) f1) false) ) +:assumption (forall (?v0 S5) (?v1 S8) (iff (= (f51 (f25 (f26 f27 ?v0) ?v1)) f1) false) ) +:assumption (forall (?v0 S15) (?v1 S5) (iff (= (f50 (f21 (f22 f23 ?v0) ?v1)) f1) false) ) +:assumption (forall (?v0 S2) (iff (= (f3 (f4 f52 ?v0) f16) f1) (= (f49 ?v0) f1)) ) +:assumption (forall (?v0 S5) (iff (= (f6 (f7 f53 ?v0) f20) f1) (= (f50 ?v0) f1)) ) +:assumption (forall (?v0 S8) (iff (= (f9 (f10 f54 ?v0) f24) f1) (= (f51 ?v0) f1)) ) +:assumption (forall (?v0 S11) (?v1 S2) (= (f55 f56 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) ?v0 (f55 f56 ?v1))) ) +:assumption (forall (?v0 S15) (?v1 S5) (= (f57 f58 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) ?v0 (f57 f58 ?v1))) ) +:assumption (forall (?v0 S5) (?v1 S8) (= (f59 f60 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) ?v0 (f59 f60 ?v1))) ) +:assumption (forall (?v0 S2) (?v1 S11) (implies (not (= ?v0 f16)) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) (f55 f56 ?v0))) ) +:assumption (forall (?v0 S5) (?v1 S15) (implies (not (= ?v0 f20)) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) (f57 f58 ?v0))) ) +:assumption (forall (?v0 S8) (?v1 S5) (implies (not (= ?v0 f24)) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) (f59 f60 ?v0))) ) +:assumption (forall (?v0 S2) (?v1 S11) (implies (= ?v0 f16) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) ?v1)) ) +:assumption (forall (?v0 S5) (?v1 S15) (implies (= ?v0 f20) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) ?v1)) ) +:assumption (forall (?v0 S8) (?v1 S5) (implies (= ?v0 f24) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) ?v1)) ) +:assumption (forall (?v0 S11) (iff (= (f61 (f62 f16) ?v0) f1) false) ) +:assumption (forall (?v0 S15) (iff (= (f63 (f64 f20) ?v0) f1) false) ) +:assumption (forall (?v0 S5) (iff (= (f6 (f65 f24) ?v0) f1) false) ) +:assumption (forall (?v0 S35) (iff (= (f3 (f66 ?v0) f16) f1) false) ) +:assumption (forall (?v0 S36) (iff (= (f6 (f67 ?v0) f20) f1) false) ) +:assumption (forall (?v0 S6) (iff (= (f9 (f68 ?v0) f24) f1) false) ) +:assumption (forall (?v0 S11) (?v1 S2) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v0) ?v1)) f1) ) +:assumption (forall (?v0 S5) (?v1 S8) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v0) ?v1)) f1) ) +:assumption (forall (?v0 S15) (?v1 S5) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v0) ?v1)) f1) ) +:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (iff (= (f61 (f62 (f17 (f18 f19 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f61 (f62 ?v1) ?v2) f1))) ) +:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (iff (= (f6 (f65 (f25 (f26 f27 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f6 (f65 ?v1) ?v2) f1))) ) +:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (iff (= (f63 (f64 (f21 (f22 f23 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f63 (f64 ?v1) ?v2) f1))) ) +:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (= (f17 f72 f16) f16) +:assumption (= (f21 f73 f20) f20) +:assumption (= (f25 f74 f24) f24) +:assumption (forall (?v0 S11) (?v1 S2) (= (f17 f72 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) f16 (f17 (f18 f19 ?v0) (f17 f72 ?v1)))) ) +:assumption (forall (?v0 S15) (?v1 S5) (= (f21 f73 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) f20 (f21 (f22 f23 ?v0) (f21 f73 ?v1)))) ) +:assumption (forall (?v0 S5) (?v1 S8) (= (f25 f74 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) f24 (f25 (f26 f27 ?v0) (f25 f74 ?v1)))) ) +:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (implies (= (f3 (f69 ?v0) ?v1) f1) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v2) ?v1)) f1)) ) +:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (implies (= (f9 (f70 ?v0) ?v1) f1) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v2) ?v1)) f1)) ) +:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (implies (= (f6 (f71 ?v0) ?v1) f1) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v2) ?v1)) f1)) ) +:assumption (forall (?v0 S2) (implies (not (= ?v0 f16)) (= (f17 (f28 f75 (f17 f72 ?v0)) (f17 (f18 f19 (f55 f56 ?v0)) f16)) ?v0)) ) +:assumption (forall (?v0 S5) (implies (not (= ?v0 f20)) (= (f21 (f30 f76 (f21 f73 ?v0)) (f21 (f22 f23 (f57 f58 ?v0)) f20)) ?v0)) ) +:assumption (forall (?v0 S8) (implies (not (= ?v0 f24)) (= (f25 (f32 f77 (f25 f74 ?v0)) (f25 (f26 f27 (f59 f60 ?v0)) f24)) ?v0)) ) +:assumption (forall (?v0 S2) (?v1 S11) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16)) ?v2) (and (not (= ?v2 f16)) (and (= (f17 f72 ?v2) ?v0) (= (f55 f56 ?v2) ?v1)))) ) +:assumption (forall (?v0 S5) (?v1 S15) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20)) ?v2) (and (not (= ?v2 f20)) (and (= (f21 f73 ?v2) ?v0) (= (f57 f58 ?v2) ?v1)))) ) +:assumption (forall (?v0 S8) (?v1 S5) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24)) ?v2) (and (not (= ?v2 f24)) (and (= (f25 f74 ?v2) ?v0) (= (f59 f60 ?v2) ?v1)))) ) +:assumption (= f11 f54) +:assumption (= f8 f53) +:assumption (= f5 f52) +:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S8) (iff (= (f9 (f10 f54 ?v0) ?v0) f1) true) ) +:assumption (forall (?v0 S5) (iff (= (f6 (f7 f53 ?v0) ?v0) f1) true) ) +:assumption (forall (?v0 S2) (iff (= (f3 (f4 f52 ?v0) ?v0) f1) true) ) +:assumption (= f54 f11) +:assumption (= f53 f8) +:assumption (= f52 f5) +:assumption (forall (?v0 S11) (?v1 S2) (iff (= (f3 (f69 ?v0) ?v1) f1) (or (exists (?v2 S11) (?v3 S2) (and (= ?v0 ?v2) (= ?v1 (f17 (f18 f19 ?v2) ?v3)))) (exists (?v2 S11) (?v3 S2) (?v4 S11) (and (= ?v0 ?v2) (and (= ?v1 (f17 (f18 f19 ?v4) ?v3)) (= (f3 (f69 ?v2) ?v3) f1)))))) ) +:assumption (forall (?v0 S5) (?v1 S8) (iff (= (f9 (f70 ?v0) ?v1) f1) (or (exists (?v2 S5) (?v3 S8) (and (= ?v0 ?v2) (= ?v1 (f25 (f26 f27 ?v2) ?v3)))) (exists (?v2 S5) (?v3 S8) (?v4 S5) (and (= ?v0 ?v2) (and (= ?v1 (f25 (f26 f27 ?v4) ?v3)) (= (f9 (f70 ?v2) ?v3) f1)))))) ) +:assumption (forall (?v0 S15) (?v1 S5) (iff (= (f6 (f71 ?v0) ?v1) f1) (or (exists (?v2 S15) (?v3 S5) (and (= ?v0 ?v2) (= ?v1 (f21 (f22 f23 ?v2) ?v3)))) (exists (?v2 S15) (?v3 S5) (?v4 S15) (and (= ?v0 ?v2) (and (= ?v1 (f21 (f22 f23 ?v4) ?v3)) (= (f6 (f71 ?v2) ?v3) f1)))))) ) +:assumption (forall (?v0 S2) (?v1 S11) (= (f55 f56 (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16))) ?v1) ) +:assumption (forall (?v0 S5) (?v1 S15) (= (f57 f58 (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20))) ?v1) ) +:assumption (forall (?v0 S8) (?v1 S5) (= (f59 f60 (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24))) ?v1) ) +:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8) (implies (= (f25 (f32 f77 ?v0) ?v1) ?v2) (implies (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 (f32 f77 ?v0) ?v3) (f25 (f32 f77 ?v2) ?v4)))) ) +:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5) (implies (= (f21 (f30 f76 ?v0) ?v1) ?v2) (implies (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 (f30 f76 ?v0) ?v3) (f21 (f30 f76 ?v2) ?v4)))) ) +:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2) (implies (= (f17 (f28 f75 ?v0) ?v1) ?v2) (implies (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 (f28 f75 ?v0) ?v3) (f17 (f28 f75 ?v2) ?v4)))) ) +:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v1)) (= ?v0 ?v2)) ) +:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v1)) (= ?v0 ?v2)) ) +:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v1)) (= ?v0 ?v2)) ) +:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v0) ?v2)) (= ?v1 ?v2)) ) +:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v0) ?v2)) (= ?v1 ?v2)) ) +:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v0) ?v2)) (= ?v1 ?v2)) ) +:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v3)) (exists (?v4 S8) (or (and (= ?v0 (f25 (f32 f77 ?v2) ?v4)) (= (f25 (f32 f77 ?v4) ?v1) ?v3)) (and (= (f25 (f32 f77 ?v0) ?v4) ?v2) (= ?v1 (f25 (f32 f77 ?v4) ?v3)))))) ) +:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v3)) (exists (?v4 S5) (or (and (= ?v0 (f21 (f30 f76 ?v2) ?v4)) (= (f21 (f30 f76 ?v4) ?v1) ?v3)) (and (= (f21 (f30 f76 ?v0) ?v4) ?v2) (= ?v1 (f21 (f30 f76 ?v4) ?v3)))))) ) +:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v3)) (exists (?v4 S2) (or (and (= ?v0 (f17 (f28 f75 ?v2) ?v4)) (= (f17 (f28 f75 ?v4) ?v1) ?v3)) (and (= (f17 (f28 f75 ?v0) ?v4) ?v2) (= ?v1 (f17 (f28 f75 ?v4) ?v3)))))) ) +:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (= (f25 (f32 f77 (f25 (f32 f77 ?v0) ?v1)) ?v2) (f25 (f32 f77 ?v0) (f25 (f32 f77 ?v1) ?v2))) ) +:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (= (f21 (f30 f76 (f21 (f30 f76 ?v0) ?v1)) ?v2) (f21 (f30 f76 ?v0) (f21 (f30 f76 ?v1) ?v2))) ) +:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (= (f17 (f28 f75 (f17 (f28 f75 ?v0) ?v1)) ?v2) (f17 (f28 f75 ?v0) (f17 (f28 f75 ?v1) ?v2))) ) +:assumption (forall (?v0 S11) (?v1 S2) (?v2 S2) (= (f17 (f28 f75 (f17 (f18 f19 ?v0) ?v1)) ?v2) (f17 (f18 f19 ?v0) (f17 (f28 f75 ?v1) ?v2))) ) +:assumption (forall (?v0 S5) (?v1 S8) (?v2 S8) (= (f25 (f32 f77 (f25 (f26 f27 ?v0) ?v1)) ?v2) (f25 (f26 f27 ?v0) (f25 (f32 f77 ?v1) ?v2))) ) +:assumption (forall (?v0 S15) (?v1 S5) (?v2 S5) (= (f21 (f30 f76 (f21 (f22 f23 ?v0) ?v1)) ?v2) (f21 (f22 f23 ?v0) (f21 (f30 f76 ?v1) ?v2))) ) +:assumption (forall (?v0 S11) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2) (implies (= (f17 (f18 f19 ?v0) ?v1) ?v2) (implies (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 (f18 f19 ?v0) ?v3) (f17 (f28 f75 ?v2) ?v4)))) ) +:assumption (forall (?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8) (implies (= (f25 (f26 f27 ?v0) ?v1) ?v2) (implies (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 (f26 f27 ?v0) ?v3) (f25 (f32 f77 ?v2) ?v4)))) ) +:assumption (forall (?v0 S15) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5) (implies (= (f21 (f22 f23 ?v0) ?v1) ?v2) (implies (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 (f22 f23 ?v0) ?v3) (f21 (f30 f76 ?v2) ?v4)))) ) +:assumption (forall (?v0 S2) (= (f17 (f28 f75 f16) ?v0) ?v0) ) +:assumption (forall (?v0 S5) (= (f21 (f30 f76 f20) ?v0) ?v0) ) +:assumption (forall (?v0 S8) (= (f25 (f32 f77 f24) ?v0) ?v0) ) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= f16 (f17 (f28 f75 ?v0) ?v1)) (and (= ?v0 f16) (= ?v1 f16))) ) +:assumption (forall (?v0 S5) (?v1 S5) (iff (= f20 (f21 (f30 f76 ?v0) ?v1)) (and (= ?v0 f20) (= ?v1 f20))) ) +:assumption (forall (?v0 S8) (?v1 S8) (iff (= f24 (f25 (f32 f77 ?v0) ?v1)) (and (= ?v0 f24) (= ?v1 f24))) ) +:assumption (forall (?v0 S2) (= (f17 (f28 f75 ?v0) f16) ?v0) ) +:assumption (forall (?v0 S5) (= (f21 (f30 f76 ?v0) f20) ?v0) ) +:assumption (forall (?v0 S8) (= (f25 (f32 f77 ?v0) f24) ?v0) ) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= ?v0 (f17 (f28 f75 ?v0) ?v1)) (= ?v1 f16)) ) +:assumption (forall (?v0 S5) (?v1 S5) (iff (= ?v0 (f21 (f30 f76 ?v0) ?v1)) (= ?v1 f20)) ) +:assumption (forall (?v0 S8) (?v1 S8) (iff (= ?v0 (f25 (f32 f77 ?v0) ?v1)) (= ?v1 f24)) ) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= ?v0 (f17 (f28 f75 ?v1) ?v0)) (= ?v1 f16)) ) +:assumption (forall (?v0 S5) (?v1 S5) (iff (= ?v0 (f21 (f30 f76 ?v1) ?v0)) (= ?v1 f20)) ) +:assumption (forall (?v0 S8) (?v1 S8) (iff (= ?v0 (f25 (f32 f77 ?v1) ?v0)) (= ?v1 f24)) ) +:assumption (forall (?v0 S26) (= (f41 f42 (f78 f79 ?v0)) ?v0)) +:assumption (forall (?v0 Int) (implies (<= 0 ?v0) (= (f78 f79 (f41 f42 ?v0)) ?v0))) +:assumption (forall (?v0 Int) (implies (< ?v0 0) (= (f78 f79 (f41 f42 ?v0)) 0))) +:formula true) +; solver: z3 +; timeout: 5.0 +; random seed: 1 +; arguments: +; DISPLAY_PROOF=true +; PROOF_MODE=2 +; -rs:1 +; MODEL=true +; -smt diff --git a/test/regress/regress0/fmf/Hoare-z3.931718.smt b/test/regress/regress0/fmf/Hoare-z3.931718.smt new file mode 100644 index 000000000..0b6fd0349 --- /dev/null +++ b/test/regress/regress0/fmf/Hoare-z3.931718.smt @@ -0,0 +1,50 @@ +% COMMAND-LINE: --finite-model-find +% EXPECT: sat +% EXIT: 10 +(benchmark Isabelle +:status sat +:logic AUFLIA +:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11) +:extrafuns ( + (f1 S1) + (f2 S1) + (f3 S3 S2 S1) + (f4 S4 S2 S3) + (f5 S4) + (f6 S5 S5 S1) + (f7 S5) + (f8 S6 S5 S5) + (f9 S7 S6) + (f10 S8 S4 S7) + (f11 S9 S10 S8) + (f12 S11 S4 S9) + (f13 S11) + (f14 S4) + (f15 S10) + (f16 S4) + (f17 S10 S4) + (f18 S5 S5 S1) +) +:assumption (not (= f1 f2)) +:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ) +:assumption (not (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1)) +:assumption (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f5) f15) (f17 f15))) f7)) f1) +:assumption (= (f18 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1) +:assumption (forall (?v0 S5) (= (f6 ?v0 f7) f1) ) +:assumption (forall (?v0 S4) (?v1 S10) (?v2 S4) (?v3 S4) (?v4 S10) (?v5 S4) (iff (= (f10 (f11 (f12 f13 ?v0) ?v1) ?v2) (f10 (f11 (f12 f13 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ) +:assumption (forall (?v0 S5) (?v1 S5) (implies (= (f6 ?v0 ?v1) f1) (= (f18 ?v0 ?v1) f1)) ) +:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (implies (= (f6 ?v0 ?v1) f1) (implies (= (f6 ?v2 ?v0) f1) (= (f6 ?v2 ?v1) f1))) ) +:assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (implies (= (f6 ?v0 ?v2) f1) (= (f6 ?v0 (f8 (f9 ?v1) ?v2)) f1))) ) +:assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) ?v2)) f1) (and (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (= (f6 ?v0 ?v2) f1))) ) +:assumption (forall (?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4) (implies (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (implies (forall (?v5 S2) (?v6 S2) (implies (= (f3 (f4 ?v3 ?v5) ?v6) f1) (= (f3 (f4 ?v4 ?v5) ?v6) f1))) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v4)) f7)) f1))) ) +:assumption (forall (?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4) (implies (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (implies (forall (?v5 S2) (?v6 S2) (implies (= (f3 (f4 ?v4 ?v5) ?v6) f1) (= (f3 (f4 ?v1 ?v5) ?v6) f1))) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v4) ?v2) ?v3)) f7)) f1))) ) +:formula true) +; solver: z3 +; timeout: 5.0 +; random seed: 1 +; arguments: +; DISPLAY_PROOF=true +; PROOF_MODE=2 +; -rs:1 +; MODEL=true +; -smt diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am new file mode 100755 index 000000000..a367447c9 --- /dev/null +++ b/test/regress/regress0/fmf/Makefile.am @@ -0,0 +1,47 @@ +BINARY = cvc4 +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + agree466.smt2 \ + ALG008-1.smt2 \ + german169.smt2 \ + Hoare-z3.931718.smt \ + QEpres-uf.855035.smt \ + agree467.smt2 \ + Arrow_Order-smtlib.778341.smt \ + german73.smt2 \ + PUZ001+1.smt2 \ + refcount24.cvc.smt2 + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 new file mode 100644 index 000000000..4bcbf51c6 --- /dev/null +++ b/test/regress/regress0/fmf/PUZ001+1.smt2 @@ -0,0 +1,119 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +; EXIT: 20 +;%------------------------------------------------------------------------------ +;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. +;% Domain : Puzzles +;% Problem : Dreadbury Mansion +;% Version : Especial. +;% Theorem formulation : Reduced > Complete. +;% English : Someone who lives in Dreadbury Mansion killed Aunt Agatha. +;% Agatha, the butler, and Charles live in Dreadbury Mansion, +;% and are the only people who live therein. A killer always +;% hates his victim, and is never richer than his victim. +;% Charles hates no one that Aunt Agatha hates. Agatha hates +;% everyone except the butler. The butler hates everyone not +;% richer than Aunt Agatha. The butler hates everyone Aunt +;% Agatha hates. No one hates everyone. Agatha is not the +;% butler. Therefore : Agatha killed herself. + +;% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au +;% : [Hah94] Haehnle (1994), Email to G. Sutcliffe +;% Source : [Hah94] +;% Names : Pelletier 55 [Pel86] + +;% Status : Theorem +;% Rating : 0.07 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0 +;% Syntax : Number of formulae : 14 ( 6 unit) +;% Number of atoms : 24 ( 5 equality) +;% Maximal formula depth : 5 ( 3 average) +;% Number of connectives : 16 ( 6 ~; 2 |; 1 &) +;% ( 0 <=>; 7 =>; 0 <=; 0 <~>) +;% ( 0 ~|; 0 ~&) +;% Number of predicates : 5 ( 0 propositional; 1-2 arity) +;% Number of functors : 3 ( 3 constant; 0-0 arity) +;% Number of variables : 12 ( 0 sgn; 10 !; 2 ?) +;% Maximal term depth : 1 ( 1 average) +;% SPC : FOF_THM_RFO_SEQ + +;% Comments : Modified by Geoff Sutcliffe. +;% : Also known as "Who killed Aunt Agatha" +;%------------------------------------------------------------------------------ +;%----Problem axioms +(set-logic UF) +(set-info :status unsat) +(declare-sort sort__smt2 0) +; functions +(declare-fun agatha__smt2_0 ( ) sort__smt2) +(declare-fun butler__smt2_0 ( ) sort__smt2) +(declare-fun charles__smt2_0 ( ) sort__smt2) +; predicates +(declare-fun lives__smt2_1 ( sort__smt2 ) Bool) +(declare-fun killed__smt2_2 ( sort__smt2 sort__smt2 ) Bool) +(declare-fun hates__smt2_2 ( sort__smt2 sort__smt2 ) Bool) +(declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool) + +; pel55_1 axiom +(assert (exists ((?X sort__smt2)) + (and (lives__smt2_1 ?X) + (killed__smt2_2 ?X agatha__smt2_0)))) + +; pel55_2_1 axiom +(assert (lives__smt2_1 agatha__smt2_0)) + +; pel55_2_2 axiom +(assert (lives__smt2_1 butler__smt2_0)) + +; pel55_2_3 axiom +(assert (lives__smt2_1 charles__smt2_0)) + +; pel55_3 axiom +(assert (forall ((?X sort__smt2)) + (=> (lives__smt2_1 ?X) + (or (= ?X agatha__smt2_0) + (= ?X butler__smt2_0) + (= ?X charles__smt2_0))))) + +; pel55_4 axiom +(assert (forall ((?X sort__smt2) (?Y sort__smt2)) + (=> (killed__smt2_2 ?X ?Y) + (hates__smt2_2 ?X ?Y)))) + +; pel55_5 axiom +(assert (forall ((?X sort__smt2) (?Y sort__smt2)) + (=> (killed__smt2_2 ?X ?Y) + (not (richer__smt2_2 ?X ?Y))))) + +; pel55_6 axiom +(assert (forall ((?X sort__smt2)) + (=> (hates__smt2_2 agatha__smt2_0 ?X) + (not (hates__smt2_2 charles__smt2_0 ?X))))) + +; pel55_7 axiom +(assert (forall ((?X sort__smt2)) + (=> (not (= ?X butler__smt2_0)) + (hates__smt2_2 agatha__smt2_0 ?X)))) + +; pel55_8 axiom +(assert (forall ((?X sort__smt2)) + (=> (not (richer__smt2_2 ?X agatha__smt2_0)) + (hates__smt2_2 butler__smt2_0 ?X)))) + +; pel55_9 axiom +(assert (forall ((?X sort__smt2)) + (=> (hates__smt2_2 agatha__smt2_0 ?X) + (hates__smt2_2 butler__smt2_0 ?X)))) + +; pel55_10 axiom +(assert (forall ((?X sort__smt2)) +(exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y))))) + +; pel55_11 axiom +(assert (not (= agatha__smt2_0 butler__smt2_0))) + +;----This is the conjecture with negated conjecture +; pel55 conjecture +(assert (not (killed__smt2_2 agatha__smt2_0 agatha__smt2_0))) + + +(check-sat) diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt new file mode 100644 index 000000000..95ab0cb34 --- /dev/null +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -0,0 +1,85 @@ +% COMMAND-LINE: --finite-model-find +% EXPECT: sat +% EXIT: 10 +(benchmark Isabelle +:status sat +:logic AUFLIA +:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18) +:extrafuns ( + (f1 S1) + (f2 S1) + (f3 S2 S3 S4) + (f4 S2) + (f5 S3) + (f6 S4) + (f7 S3 S5 S1) + (f8 S6 S5) + (f9 S6) + (f10 S7 S6 S6) + (f11 S7) + (f12 S8 S4 S4) + (f13 S8) + (f14 S10 S3 S3) + (f15 S11 S9 S10) + (f16 S12 S4 S11) + (f17 S12) + (f18 S4 S13 S1) + (f19 S13) + (f20 S4 S1) + (f21 S2) + (f22 S10) + (f23 S3 S9 S1) + (f24 S14 S9 S9) + (f25 S15 S4 S14) + (f26 S15) + (f27 S13) + (f28 S8) + (f29 S16 S9 S3) + (f30 S17 S4 S16) + (f31 S18 S4 S17) + (f32 S18) + (f33 S18) + (f34 S4 S4 S1) +) +:assumption (not (= f1 f2)) +:assumption (not (not (= (f3 f4 f5) f6))) +:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f4 ?v0) f6))) ) +:assumption (= (f7 f5 (f8 (f10 f11 f9))) f1) +:assumption (forall (?v0 S4) (iff (= f6 ?v0) (= ?v0 f6)) ) +:assumption (= (f12 f13 f6) f6) +:assumption (forall (?v0 S4) (iff (= f6 (f12 f13 ?v0)) (= ?v0 f6)) ) +:assumption (forall (?v0 S4) (iff (= (f12 f13 ?v0) f6) (= ?v0 f6)) ) +:assumption (forall (?v0 S4) (?v1 S9) (?v2 S3) (= (f3 f4 (f14 (f15 (f16 f17 ?v0) ?v1) ?v2)) (f3 f4 ?v2)) ) +:assumption (= (f18 f6 f19) f1) +:assumption (= (f20 f6) f1) +:assumption (forall (?v0 S4) (iff (= (f20 ?v0) f1) (= ?v0 f6)) ) +:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f21 ?v0) f6))) ) +:assumption (forall (?v0 S3) (implies (not (not (= (f3 f21 ?v0) f6))) (implies (not (= (f3 f4 ?v0) f6)) (not (= (f3 f4 (f14 f22 ?v0)) f6)))) ) +:assumption (forall (?v0 S4) (?v1 S4) (iff (= (f12 f13 ?v0) (f12 f13 ?v1)) (= ?v0 ?v1)) ) +:assumption (forall (?v0 S6) (?v1 S9) (implies (forall (?v2 S3) (implies (= (f7 ?v2 (f8 ?v0)) f1) (not (= (f3 f21 ?v2) f6)))) (iff (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 (f10 f11 ?v0))) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))) (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 ?v0)) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))))) ) +:assumption (forall (?v0 S4) (= (f18 (f12 f13 ?v0) f27) f1) ) +:assumption (= (f12 f28 f6) f6) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f32 ?v0) ?v1) ?v2)) ?v0) ) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f33 ?v0) ?v1) ?v2)) ?v0) ) +:assumption (= (f18 f6 f27) f1) +:assumption (forall (?v0 S3) (?v1 S4) (?v2 S9) (implies (not (not (= (f3 f21 ?v0) f6))) (iff (= (f23 ?v0 (f24 (f25 f26 ?v1) ?v2)) f1) (= (f23 (f14 f22 ?v0) ?v2) f1))) ) +:assumption (forall (?v0 S4) (iff (= (f34 (f12 f13 ?v0) f6) f1) (= (f34 ?v0 f6) f1)) ) +:assumption (forall (?v0 S4) (iff (= (f34 f6 (f12 f13 ?v0)) f1) (= (f34 f6 ?v0) f1)) ) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (not (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5))) ) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (not (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5))) ) +:assumption (forall (?v0 S4) (= (f34 ?v0 ?v0) f1) ) +:assumption (forall (?v0 S4) (?v1 S4) (or (= (f34 ?v0 ?v1) f1) (= (f34 ?v1 ?v0) f1)) ) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ) +:assumption (forall (?v0 S4) (?v1 S4) (?v2 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v2) f1) (= (f34 ?v0 ?v2) f1))) ) +:assumption (forall (?v0 S4) (?v1 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v0) f1) (= ?v0 ?v1))) ) +:formula true) +; solver: z3 +; timeout: 1.897 +; random seed: 1 +; arguments: +; DISPLAY_PROOF=true +; PROOF_MODE=2 +; -rs:1 +; MODEL=true +; -smt diff --git a/test/regress/regress0/fmf/agree466.smt2 b/test/regress/regress0/fmf/agree466.smt2 new file mode 100644 index 000000000..2a021ea9b --- /dev/null +++ b/test/regress/regress0/fmf/agree466.smt2 @@ -0,0 +1,475 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +; Preamble -------------- +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort value$type 0) +(define-sort Nodes$elem$type () node$type) +(declare-sort Nodes$t$type 0) +(declare-fun Nodes$empty () Nodes$t$type) +(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL) +(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$cardinality (Nodes$t$type) Int) +(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$disjoint_empty : +(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth))) +;Nodes$disjoint_comm : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b) + (Nodes$disjoint b a)))) +;Nodes$mem_empty : +(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty) + Truth)))) +;Nodes$mem_add : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s) + Truth)) Truth + Falsity)))) +;Nodes$mem_remove : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (= + (Nodes$mem + x s) + Truth)) + Truth Falsity)))) +;Nodes$mem_union1 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a) + Truth) (forall + ((b Nodes$t$type)) + (= + (Nodes$mem + x (Nodes$union + a b)) + Truth))))) +;Nodes$mem_union2 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b) + (Nodes$union b a)))) +;Nodes$mem_union3 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type)) + (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a) + Truth) (= (Nodes$mem + x b) + Truth))))) +;Nodes$mem_union4 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a))) +;Nodes$mem_union5 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a))) +;Nodes$empty_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b) + Nodes$empty) + (= a Nodes$empty)))) +;Nodes$card_empty : +(assert (= (Nodes$cardinality Nodes$empty) 0)) +;Nodes$card_zero : +(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (= + s + Nodes$empty)))) +;Nodes$card_non_negative : +(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0))) +;Nodes$card_add : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$add x s)) + (ite (= (Nodes$mem + x s) Truth) + (Nodes$cardinality + s) (+ (Nodes$cardinality + s) 1))))) +;Nodes$card_remove : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$remove x s)) + (ite (= (Nodes$mem + x s) Truth) (- + (Nodes$cardinality + s) 1) (Nodes$cardinality + s))))) +;Nodes$card_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint + a b) Truth) + (= (Nodes$cardinality + (Nodes$union a b)) (+ + (Nodes$cardinality + a) (Nodes$cardinality b)))))) +(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$eq_is_equality : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b) + (ite (= a b) Truth + Falsity)))) +;Nodes$equal1 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type)) + (= (Nodes$mem x a) + (Nodes$mem x b))) + (= (Nodes$eq a b) + Truth)))) +(define-sort Values$elem$type () value$type) +(declare-sort Values$t$type 0) +(declare-fun Values$empty () Values$t$type) +(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL) +(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$cardinality (Values$t$type) Int) +(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type) +(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL) +;Values$disjoint_empty : +(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty) + Truth))) +;Values$disjoint_comm : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint + a b) (Values$disjoint + b a)))) +;Values$mem_empty : +(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty) + Truth)))) +;Values$mem_add : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem + x s) Truth)) + Truth Falsity)))) +;Values$mem_remove : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y)) + (= (Values$mem x s) + Truth)) Truth Falsity)))) +;Values$mem_union1 : +(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem + x a) + Truth) (forall + ( + (b Values$t$type)) + (= + (Values$mem + x + (Values$union + a b)) + Truth))))) +;Values$mem_union2 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b) + (Values$union b a)))) +;Values$mem_union3 : +(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type)) + (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem + x a) Truth) + (= (Values$mem x b) + Truth))))) +;Values$mem_union4 : +(assert (forall ((a Values$t$type)) (= (Values$union a a) a))) +;Values$mem_union5 : +(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a))) +;Values$empty_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union + a b) Values$empty) + (= a Values$empty)))) +;Values$card_empty : +(assert (= (Values$cardinality Values$empty) 0)) +;Values$card_zero : +(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0) + (= s Values$empty)))) +;Values$card_non_negative : +(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0))) +;Values$card_add : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$add x s)) + (ite (= (Values$mem + x s) + Truth) + (Values$cardinality + s) (+ (Values$cardinality + s) 1))))) +;Values$card_remove : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$remove + x s)) (ite + (= + (Values$mem + x s) + Truth) (- + (Values$cardinality + s) + 1) + (Values$cardinality + s))))) +;Values$card_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint + a b) Truth) + (= (Values$cardinality + (Values$union a b)) (+ + (Values$cardinality + a) (Values$cardinality + b)))))) +(declare-fun Values$eq (Values$t$type Values$t$type) BOOL) +;Values$eq_is_equality : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b) + (ite (= a b) Truth + Falsity)))) +;Values$equal1 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type)) + (= (Values$mem x a) + (Values$mem + x b))) (= (Values$eq + a b) + Truth)))) +(define-sort node_set$type () (Array node$type BOOL)) +(declare-fun mk_array_1 () (Array node$type BOOL)) +;mk_array_1_def : +(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1 + mk_array_1_index) Falsity))) +(define-fun empty_node_set () node_set$type mk_array_1) +(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL))) +(declare-fun mk_array_2 () (Array node$type BOOL)) +;mk_array_2_def : +(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2 + mk_array_2_index) Falsity))) +(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL))) +;mk_array_3_def : +(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3 + mk_array_3_index) mk_array_2))) +(define-fun empty_node_pair_set () node_pair_set$type mk_array_3) +(declare-fun mk_array_4 () (Array node$type BOOL)) +;mk_array_4_def : +(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4 + mk_array_4_index) Truth))) +(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL))) +;mk_array_5_def : +(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5 + mk_array_5_index) mk_array_4))) +(define-fun full_node_pair_set () node_pair_set$type mk_array_5) +(declare-fun input () (Array node$type value$type)) +(declare-fun t () Int) +;positive_bound : +(assert (> t 0)) +(define-sort message$type () Values$t$type) +(define-sort message_set$type () (Array node$type message$type)) +(define-sort state$type () Values$t$type) +(define-sort state_set$type () (Array node$type state$type)) +(define-fun null_message () message$type Values$empty) +(declare-fun mk_array_6 () (Array node$type message$type)) +;mk_array_6_def : +(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6 + mk_array_6_index) null_message))) +(define-fun null_message_set () message_set$type mk_array_6) +(define-fun null_state () state$type Values$empty) +(declare-fun mk_array_7 () (Array node$type state$type)) +;mk_array_7_def : +(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7 + mk_array_7_index) null_state))) +(define-fun null_state_set () state_set$type mk_array_7) +(declare-fun choose (Values$t$type) value$type) +;choosen_value : +(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem + (choose + vals) + vals) + Truth)))) +(define-sort failure_pattern$type () node_pair_set$type) +(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase)))) +(declare-datatypes () ((clean_state$type (before) (active) (after)))) + +; Var Decls -------------- +(declare-fun my_compute$result$1 () state$type) +(declare-fun output$1 () (Array node$type value$type)) +(declare-fun comp_done () node_set$type) +(declare-fun compute$can_decide$0$1 () BOOL) +(declare-fun chosen () (Array node$type BOOL)) +(declare-fun recv_done () node_pair_set$type) +(declare-fun output () (Array node$type value$type)) +(declare-fun phase () phase_state$type) +(declare-fun global_state () state_set$type) +(declare-fun my_decide$result$1 () value$type) +(declare-fun round () Int) +(declare-fun compute$n () node$type) +(declare-fun send_done () node_pair_set$type) +(declare-fun my_can_decide$result$1 () BOOL) +(declare-fun chosen$1 () (Array node$type BOOL)) +(declare-fun comp_done$1 () node_set$type) +(declare-fun global_state$1 () state_set$type) + +; Asserts -------------- +(assert (not (=> (forall ((n node$type)) (=> + (and + (= + (select + chosen + n) + Truth) + (= + round (+ + t + 1))) + (and + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + send_done + n) + m) + Truth)) + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + recv_done + n) + m) + Truth))))) + (=> (= phase comp_phase) (=> + (not + (= (select + comp_done + compute$n) + Truth)) + (=> + (= my_compute$result$1 + (select + global_state + compute$n)) + (=> + (= global_state$1 + (store + global_state + compute$n + my_compute$result$1)) + (=> + (= my_can_decide$result$1 + (ite + (= round (+ + t 1)) + Truth + Falsity)) + (=> + (= compute$can_decide$0$1 + my_can_decide$result$1) + (= (ite + (= + compute$can_decide$0$1 + Truth) + (ite + (=> + (= + my_decide$result$1 + (choose + (select + global_state$1 + compute$n))) + (=> + (= + output$1 + (store + output + compute$n + my_decide$result$1)) + (=> + (= + chosen$1 + (store + chosen + compute$n + Truth)) + (=> + (= + comp_done$1 + (store + comp_done + compute$n + Truth)) + (forall + ( + (n node$type)) + (=> + (and + (= + (select + chosen$1 + n) + Truth) + (= + round (+ + t + 1))) + (and + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + send_done + n) + m) + Truth)) + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + recv_done + n) + m) + Truth))))))))) + Truth + Falsity) + (ite + (=> + (= + comp_done$1 + (store + comp_done + compute$n + Truth)) + (forall + ( + (n node$type)) + (=> + (and + (= + (select + chosen + n) + Truth) + (= + round (+ + t + 1))) + (and + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + send_done + n) + m) + Truth)) + (forall + ( + (n node$type) (m node$type)) + (= + (select + (select + recv_done + n) + m) + Truth)))))) + Truth + Falsity)) + Truth)))))))))) + +(check-sat) diff --git a/test/regress/regress0/fmf/agree467.smt2 b/test/regress/regress0/fmf/agree467.smt2 new file mode 100644 index 000000000..09e16dfe3 --- /dev/null +++ b/test/regress/regress0/fmf/agree467.smt2 @@ -0,0 +1,342 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +; EXIT: 20 +; Preamble -------------- +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort value$type 0) +(define-sort Nodes$elem$type () node$type) +(declare-sort Nodes$t$type 0) +(declare-fun Nodes$empty () Nodes$t$type) +(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL) +(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$cardinality (Nodes$t$type) Int) +(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type) +(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$disjoint_empty : +(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth))) +;Nodes$disjoint_comm : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b) + (Nodes$disjoint b a)))) +;Nodes$mem_empty : +(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty) + Truth)))) +;Nodes$mem_add : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s) + Truth)) Truth + Falsity)))) +;Nodes$mem_remove : +(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) + (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (= + (Nodes$mem + x s) + Truth)) + Truth Falsity)))) +;Nodes$mem_union1 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a) + Truth) (forall + ((b Nodes$t$type)) + (= + (Nodes$mem + x (Nodes$union + a b)) + Truth))))) +;Nodes$mem_union2 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b) + (Nodes$union b a)))) +;Nodes$mem_union3 : +(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type)) + (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a) + Truth) (= (Nodes$mem + x b) + Truth))))) +;Nodes$mem_union4 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a))) +;Nodes$mem_union5 : +(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a))) +;Nodes$empty_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b) + Nodes$empty) + (= a Nodes$empty)))) +;Nodes$card_empty : +(assert (= (Nodes$cardinality Nodes$empty) 0)) +;Nodes$card_zero : +(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (= + s + Nodes$empty)))) +;Nodes$card_non_negative : +(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0))) +;Nodes$card_add : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$add x s)) + (ite (= (Nodes$mem + x s) Truth) + (Nodes$cardinality + s) (+ (Nodes$cardinality + s) 1))))) +;Nodes$card_remove : +(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality + (Nodes$remove x s)) + (ite (= (Nodes$mem + x s) Truth) (- + (Nodes$cardinality + s) 1) (Nodes$cardinality + s))))) +;Nodes$card_union : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint + a b) Truth) + (= (Nodes$cardinality + (Nodes$union a b)) (+ + (Nodes$cardinality + a) (Nodes$cardinality b)))))) +(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL) +;Nodes$eq_is_equality : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b) + (ite (= a b) Truth + Falsity)))) +;Nodes$equal1 : +(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type)) + (= (Nodes$mem x a) + (Nodes$mem x b))) + (= (Nodes$eq a b) + Truth)))) +(define-sort Values$elem$type () value$type) +(declare-sort Values$t$type 0) +(declare-fun Values$empty () Values$t$type) +(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL) +(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type) +(declare-fun Values$cardinality (Values$t$type) Int) +(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type) +(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL) +;Values$disjoint_empty : +(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty) + Truth))) +;Values$disjoint_comm : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint + a b) (Values$disjoint + b a)))) +;Values$mem_empty : +(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty) + Truth)))) +;Values$mem_add : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem + x s) Truth)) + Truth Falsity)))) +;Values$mem_remove : +(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) + (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y)) + (= (Values$mem x s) + Truth)) Truth Falsity)))) +;Values$mem_union1 : +(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem + x a) + Truth) (forall + ( + (b Values$t$type)) + (= + (Values$mem + x + (Values$union + a b)) + Truth))))) +;Values$mem_union2 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b) + (Values$union b a)))) +;Values$mem_union3 : +(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type)) + (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem + x a) Truth) + (= (Values$mem x b) + Truth))))) +;Values$mem_union4 : +(assert (forall ((a Values$t$type)) (= (Values$union a a) a))) +;Values$mem_union5 : +(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a))) +;Values$empty_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union + a b) Values$empty) + (= a Values$empty)))) +;Values$card_empty : +(assert (= (Values$cardinality Values$empty) 0)) +;Values$card_zero : +(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0) + (= s Values$empty)))) +;Values$card_non_negative : +(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0))) +;Values$card_add : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$add x s)) + (ite (= (Values$mem + x s) + Truth) + (Values$cardinality + s) (+ (Values$cardinality + s) 1))))) +;Values$card_remove : +(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality + (Values$remove + x s)) (ite + (= + (Values$mem + x s) + Truth) (- + (Values$cardinality + s) + 1) + (Values$cardinality + s))))) +;Values$card_union : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint + a b) Truth) + (= (Values$cardinality + (Values$union a b)) (+ + (Values$cardinality + a) (Values$cardinality + b)))))) +(declare-fun Values$eq (Values$t$type Values$t$type) BOOL) +;Values$eq_is_equality : +(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b) + (ite (= a b) Truth + Falsity)))) +;Values$equal1 : +(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type)) + (= (Values$mem x a) + (Values$mem + x b))) (= (Values$eq + a b) + Truth)))) +(define-sort node_set$type () (Array node$type BOOL)) +(declare-fun mk_array_1 () (Array node$type BOOL)) +;mk_array_1_def : +(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1 + mk_array_1_index) Falsity))) +(define-fun empty_node_set () node_set$type mk_array_1) +(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL))) +(declare-fun mk_array_2 () (Array node$type BOOL)) +;mk_array_2_def : +(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2 + mk_array_2_index) Falsity))) +(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL))) +;mk_array_3_def : +(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3 + mk_array_3_index) mk_array_2))) +(define-fun empty_node_pair_set () node_pair_set$type mk_array_3) +(declare-fun mk_array_4 () (Array node$type BOOL)) +;mk_array_4_def : +(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4 + mk_array_4_index) Truth))) +(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL))) +;mk_array_5_def : +(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5 + mk_array_5_index) mk_array_4))) +(define-fun full_node_pair_set () node_pair_set$type mk_array_5) +(declare-fun input () (Array node$type value$type)) +(declare-fun t () Int) +;positive_bound : +(assert (> t 0)) +(define-sort message$type () Values$t$type) +(define-sort message_set$type () (Array node$type message$type)) +(define-sort state$type () Values$t$type) +(define-sort state_set$type () (Array node$type state$type)) +(define-fun null_message () message$type Values$empty) +(declare-fun mk_array_6 () (Array node$type message$type)) +;mk_array_6_def : +(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6 + mk_array_6_index) null_message))) +(define-fun null_message_set () message_set$type mk_array_6) +(define-fun null_state () state$type Values$empty) +(declare-fun mk_array_7 () (Array node$type state$type)) +;mk_array_7_def : +(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7 + mk_array_7_index) null_state))) +(define-fun null_state_set () state_set$type mk_array_7) +(declare-fun choose (Values$t$type) value$type) +;choosen_value : +(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem + (choose + vals) + vals) + Truth)))) +(define-sort failure_pattern$type () node_pair_set$type) +(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL +(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth))) +Truth Falsity)) +(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase)))) +(declare-datatypes () ((clean_state$type (before) (active) (after)))) + +; Var Decls -------------- +(declare-fun init_done () node_set$type) +(declare-fun crashed () Nodes$t$type) +(declare-fun comp_done () node_set$type) +(declare-fun chosen () (Array node$type BOOL)) +(declare-fun recv_done () node_pair_set$type) +(declare-fun phase () phase_state$type) +(declare-fun clean () clean_state$type) +(declare-fun global_state () state_set$type) +(declare-fun messages () (Array node$type message_set$type)) +(declare-fun deliver_message () failure_pattern$type) +(declare-fun crashing () Nodes$t$type) +(declare-fun round () Int) +(declare-fun send_done () node_pair_set$type) + +; Asserts -------------- +(declare-fun mk_array_8 () (Array node$type BOOL)) +;mk_array_8_def : +(assert (forall ((mk_array_8_index node$type)) (= (select mk_array_8 + mk_array_8_index) Falsity))) +(declare-fun mk_array_9 () (Array node$type message_set$type)) +;mk_array_9_def : +(assert (forall ((mk_array_9_index node$type)) (= (select mk_array_9 + mk_array_9_index) null_message_set))) +(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and + (and + (= + clean + before) + (= + global_state + null_state_set)) + (= + messages + mk_array_9)) + (= deliver_message + full_node_pair_set)) + (= comp_done + empty_node_set)) + (= recv_done empty_node_pair_set)) + (= send_done empty_node_pair_set)) + (= init_done empty_node_set)) + (= phase init_phase)) (= crashing + Nodes$empty)) + (= crashed Nodes$empty)) (= round 0)) (= chosen + mk_array_8)) + (forall ((n node$type)) (=> (and (= (select chosen n) Truth) + (= round (+ t 1))) (and (forall + ((n node$type) (m node$type)) + (= (select + (select + send_done + n) + m) + Truth)) + (forall ( + (n node$type) (m node$type)) + (= (select + (select + recv_done + n) m) + Truth)))))))) + +(check-sat) diff --git a/test/regress/regress0/fmf/german169.smt2 b/test/regress/regress0/fmf/german169.smt2 new file mode 100755 index 000000000..f0906d6b5 --- /dev/null +++ b/test/regress/regress0/fmf/german169.smt2 @@ -0,0 +1,104 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort data$type 0) +(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive)))) +(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type))))) +(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)))) +(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type))))) +(declare-fun dummy () data$type) + +; Var Decls -------------- +(declare-fun memdata$1 () data$type) +(declare-fun shrset$1 () (Array node$type BOOL)) +(declare-fun recv_invack$i () node$type) +(declare-fun exgntd () BOOL) +(declare-fun chan3$1 () (Array node$type msg$type)) +(declare-fun shrset () (Array node$type BOOL)) +(declare-fun exgntd$1 () BOOL) +(declare-fun chan2 () (Array node$type msg$type)) +(declare-fun chan3 () (Array node$type msg$type)) +(declare-fun auxnode () node$type) +(declare-fun curcmd () msg_cmd$type) + +; Asserts -------------- +(assert (not (=> (and (and (forall ((n node$type)) + (=> (= (m_cmd (select + chan2 + n)) + gnte) (= exgntd + Truth))) + (forall ((n node$type)) + (=> (= exgntd Truth) + (= (select shrset n) + (ite (= n auxnode) Truth + Falsity))))) (forall + ((n node$type)) + (=> (= + (m_cmd + (select + chan3 + n)) + invack) + (= (m_cmd + (select + chan2 + n)) + empty)))) + (=> (= (m_cmd (select chan3 recv_invack$i)) + invack) (=> (not (= curcmd empty)) + (=> (= chan3$1 (store + chan3 + recv_invack$i + (let ( + (vup_228 + (select + chan3 + recv_invack$i))) + (c_msg$type + empty + (m_data + vup_228))))) + (=> (= shrset$1 (store + shrset + recv_invack$i + Falsity)) + (= (ite (= exgntd Truth) + (ite (=> (= exgntd$1 + Falsity) + (=> (= memdata$1 + (m_data + (select + chan3$1 + recv_invack$i))) + (forall ( + (n node$type)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd$1 + Truth))))) + Truth Falsity) + (ite (forall ( + (n node$type)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd + Truth))) + Truth Falsity)) + Truth)))))))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/fmf/german73.smt2 b/test/regress/regress0/fmf/german73.smt2 new file mode 100755 index 000000000..388a53624 --- /dev/null +++ b/test/regress/regress0/fmf/german73.smt2 @@ -0,0 +1,106 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +; EXIT: 20 +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort data$type 0) +(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive)))) +(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type))))) +(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)))) +(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type))))) +(declare-fun dummy () data$type) + +; Var Decls -------------- +(declare-fun memdata$1 () data$type) +(declare-fun shrset$1 () (Array node$type BOOL)) +(declare-fun recv_invack$i () node$type) +(declare-fun exgntd () BOOL) +(declare-fun invset () (Array node$type BOOL)) +(declare-fun chan3$1 () (Array node$type msg$type)) +(declare-fun shrset () (Array node$type BOOL)) +(declare-fun exgntd$1 () BOOL) +(declare-fun chan2 () (Array node$type msg$type)) +(declare-fun chan3 () (Array node$type msg$type)) +(declare-fun curcmd () msg_cmd$type) + +; Asserts -------------- +(assert (not (=> (and (forall ((n node$type)) + (=> (= (select invset n) + Truth) (= (select + shrset + n) Truth))) + (forall ((n node$type)) (=> + (or + (= + (m_cmd + (select + chan2 + n)) + inv) + (= + (m_cmd + (select + chan3 + n)) + invack)) + (not + (= + (select + invset + n) + Truth))))) + (=> (= (m_cmd (select chan3 recv_invack$i)) + invack) (=> (not (= curcmd empty)) + (=> (= chan3$1 (store + chan3 + recv_invack$i + (let ( + (vup_101 + (select + chan3 + recv_invack$i))) + (c_msg$type + empty + (m_data + vup_101))))) + (=> (= shrset$1 (store + shrset + recv_invack$i + Falsity)) + (= (ite (= exgntd Truth) + (ite (=> (= exgntd$1 + Falsity) + (=> (= memdata$1 + (m_data + (select + chan3$1 + recv_invack$i))) + (forall ( + (n node$type)) + (=> (= (select + invset + n) + Truth) + (= (select + shrset$1 + n) Truth))))) + Truth Falsity) + (ite (forall ( + (n node$type)) + (=> (= (select + invset + n) + Truth) + (= (select + shrset$1 + n) Truth))) + Truth Falsity)) + Truth)))))))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/fmf/refcount24.cvc.smt2 b/test/regress/regress0/fmf/refcount24.cvc.smt2 new file mode 100755 index 000000000..bf042c9b2 --- /dev/null +++ b/test/regress/regress0/fmf/refcount24.cvc.smt2 @@ -0,0 +1,38 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic ALL_SUPPORTED) +(set-info :smt-lib-version 2.0) +(set-info :category "unknown") +(set-info :status sat) +(declare-datatypes () +((UNIT (Unit)) +)) +(declare-datatypes () +((BOOL (Truth) (Falsity)) +)) +(declare-sort resource$type 0) +(declare-sort process$type 0) +(declare-fun null () resource$type) +(declare-sort S$t$type 0) +(declare-fun S$empty () S$t$type) +(declare-fun S$mem (process$type S$t$type) BOOL) +(declare-fun S$add (process$type S$t$type) S$t$type) +(declare-fun S$remove (process$type S$t$type) S$t$type) +(declare-fun S$cardinality (S$t$type) Int) +(assert (forall ((e process$type)) (not (= (S$mem e S$empty) Truth)))) +(assert (forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$add y s)) (ite (or (= x y) (= (S$mem x s) Truth)) Truth Falsity)))) +(assert (forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$remove y s)) (ite (and (not (= x y)) (= (S$mem x s) Truth)) Truth Falsity)))) +(assert (= (S$cardinality S$empty) 0)) +(assert (forall ((s S$t$type)) (=> (= (S$cardinality s) 0) (= s S$empty)))) +(assert (forall ((s S$t$type)) (>= (S$cardinality s) 0))) +(assert (forall ((x process$type) (s S$t$type)) (let ((?v_0 (S$cardinality s))) (= (S$cardinality (S$add x s)) (ite (= (S$mem x s) Truth) ?v_0 (+ ?v_0 1)))))) +(assert (forall ((x process$type) (s S$t$type)) (let ((?v_0 (S$cardinality s))) (= (S$cardinality (S$remove x s)) (ite (= (S$mem x s) Truth) (- ?v_0 1) ?v_0))))) +(declare-fun count () (Array resource$type Int)) +(declare-fun ref () (Array process$type resource$type)) +(declare-fun valid () (Array resource$type BOOL)) +(declare-fun destroy$r () resource$type) +(declare-fun valid$1 () (Array resource$type BOOL)) +(assert (not (=> (forall ((p process$type)) (let ((?v_0 (select ref p))) (=> (not (= ?v_0 null)) (= (select valid ?v_0) Truth)))) (=> (not (= destroy$r null)) (=> (= (select valid destroy$r) Truth) (=> (= (select count destroy$r) 0) (=> (= valid$1 (store valid destroy$r Falsity)) (forall ((p process$type)) (let ((?v_1 (select ref p))) (=> (not (= ?v_1 null)) (= (select valid$1 ?v_1) Truth))))))))))) +(check-sat) +(exit) -- cgit v1.2.3