Merge branch 'master' of https://github.com/CVC4/CVC4

Conflicts:
	src/theory/arith/theory_arith_private.cpp
	src/theory/quantifiers_engine.cpp

47 files changed, 2630 insertions, 131 deletions

diff --git a/NEWS b/NEWS
index b8f1177d0..eb991f74c 100644
--- a/NEWS
+++ b/NEWS
@@ -3,7 +3,10 @@ This file contains a summary of important user-visible changes.
 Changes since 1.2
 =================
 
-* nothing yet
+* We no longer permit model or proof generation if there's been an
+  intervening push/pop.
+* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
+  resolved
 
 Changes since 1.1
 =================
diff --git a/THANKS b/THANKS
index b135fe36e..f6586d2dc 100644
--- a/THANKS
+++ b/THANKS
@@ -1,3 +1,6 @@
 Thanks to Peter Collingbourne and his group (the Multicore Programming Group
 at Imperial College London) for developing and submitting some patches in
 September 2012 related to SMT-LIBv2 compliance.
+
+Thanks to David Cok of GrammaTech, Inc., for suggesting numerous improvements
+in CVC4's SMT-LIBv2 compliance in May 2013.
diff --git a/config/bindings.m4 b/config/bindings.m4
index 6aa9b1ac5..3f75479bd 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -10,6 +10,17 @@ AC_DEFUN([CVC4_SUPPORTED_BINDINGS],
 AC_DEFUN([CVC4_ALL_BINDINGS],
 [c,java,csharp,perl,php,python,ruby,tcl,ocaml])
 
+# CVC4_NEED_SWIG_FOR_BINDING
+# --------------------------
+# Used by CVC4_CHECK_BINDINGS to ensure swig is available (and correct
+# version) when a binding needs it
+AC_DEFUN([CVC4_NEED_SWIG_FOR_BINDING], [
+  if test -z "$SWIG"; then
+    AC_MSG_WARN([swig not available or incompatible version; $binding bindings require swig 2.0.0 or later])
+    binding_error=yes
+  fi
+])
+
 # CVC4_CHECK_BINDINGS(DEFAULT_BINDINGS_LIST)
 # ------------------------------------------
 # Check for user language binding preferences, and what is possible
@@ -41,7 +52,27 @@ else
     AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", [])
   fi
   if test -z "$SWIG"; then
+    AC_MSG_RESULT([not found])
     AC_MSG_WARN([language bindings for native API disabled, swig not found.])
+  else
+    AC_MSG_CHECKING([compatibility with version of swig])
+    cat > conftest.c << _CVC4EOF
+%module conftest
+#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000
+#error bad version
+#endif
+_CVC4EOF
+    if $SWIG conftest.c >&AS_MESSAGE_LOG_FD 2>&1; then
+      AC_MSG_RESULT([compatible version])
+    else
+      AC_MSG_RESULT([incompatible version])
+      AC_MSG_WARN([swig version 2.0.0 or later is required to build native API bindings])
+      SWIG=
+      echo '===Failed swig input was:' >&AS_MESSAGE_LOG_FD
+      cat conftest.c >&AS_MESSAGE_LOG_FD
+      echo '===End failed swig input' >&AS_MESSAGE_LOG_FD
+      rm -f conftest.c
+    fi
   fi
 fi
 
@@ -78,30 +109,35 @@ for binding in $try_bindings; do
       AC_MSG_RESULT([C support will be built]);;
     java)
       AC_MSG_RESULT([Java support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(JAVA_CPPFLAGS, [flags to pass to compiler when building Java bindings])
       CPPFLAGS="$CPPFLAGS $JAVA_CPPFLAGS"
       AC_CHECK_HEADER([jni.h], [cvc4_build_java_bindings=yes], [binding_error=yes])
       ;;
     csharp)
       AC_MSG_RESULT([[C# support will be built]])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(CSHARP_CPPFLAGS, [flags to pass to compiler when building C# bindings])
       CPPFLAGS="$CPPFLAGS $CSHARP_CPPFLAGS"
       cvc4_build_csharp_bindings=yes
       ;;
     perl)
       AC_MSG_RESULT([perl support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(PERL_CPPFLAGS, [flags to pass to compiler when building perl bindings])
       CPPFLAGS="$CPPFLAGS $PERL_CPPFLAGS"
       AC_CHECK_HEADER([EXTERN.h], [cvc4_build_perl_bindings=yes], [binding_error=yes])
       ;;
     php)
       AC_MSG_RESULT([php support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(PHP_CPPFLAGS, [flags to pass to compiler when building PHP bindings])
       CPPFLAGS="$CPPFLAGS $PHP_CPPFLAGS"
       AC_CHECK_HEADER([zend.h], [cvc4_build_php_bindings=yes], [binding_error=yes])
       ;;
     python)
       AC_MSG_RESULT([python support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AM_PATH_PYTHON([2.5], [cvc4_build_python_bindings=yes], [binding_error=yes])
       AC_ARG_VAR([PYTHON_INCLUDE], [Include flags for python, bypassing python-config])
       AC_ARG_VAR([PYTHON_CONFIG], [Path to python-config])
@@ -122,18 +158,21 @@ for binding in $try_bindings; do
       ;;
     ruby)
       AC_MSG_RESULT([ruby support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(RUBY_CPPFLAGS, [flags to pass to compiler when building ruby bindings])
       CPPFLAGS="$CPPFLAGS $RUBY_CPPFLAGS"
       AC_CHECK_HEADER([ruby.h], [cvc4_build_ruby_bindings=yes], [binding_error=yes])
       ;;
     tcl)
       AC_MSG_RESULT([tcl support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building tcl bindings])
       CPPFLAGS="$CPPFLAGS $TCL_CPPFLAGS"
       AC_CHECK_HEADER([tcl.h], [cvc4_build_tcl_bindings=yes], [binding_error=yes])
       ;;
     ocaml)
       AC_MSG_RESULT([OCaml support will be built])
+      CVC4_NEED_SWIG_FOR_BINDING
       AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building OCaml bindings])
       CPPFLAGS="$CPPFLAGS $OCAML_CPPFLAGS"
       AC_CHECK_HEADER([caml/misc.h], [cvc4_build_ocaml_bindings=yes], [binding_error=yes])
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 <glpk.h>],
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
+                                  [#include <glpk/glpk.h>]
+                                  [#else]
+                                  [#include <glpk.h>]
+                                  [#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 <glpk.h>],
+  AC_LINK_IFELSE([AC_LANG_PROGRAM([#ifdef HAVE_GLPK_GLPK_H]
+                                  [#include <glpk/glpk.h>]
+                                  [#else]
+                                  [#include <glpk.h>]
+                                  [#endif],
                                   [int i = lpx_get_int_parm(NULL, LPX_K_ITCNT)])],
     [GLPK_LIBS="-lglpk $1"],
     [])
diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index 5376bfd72..2a10c5347 100755
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/run-script-casc24-fnt
@@ -12,25 +12,27 @@ filename=${file%.*}
 # which case this run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
-  result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  limit=$1; shift;
+  (ulimit -t "$limit";$cvc4 -L tptp --szs-compliant --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
+  (read result;
   case "$result" in
-    sat) echo "SZS Satisfiable for $filename"; exit 0;;
-    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
-    conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
-    conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
-  esac
-}
-function finishwith {
-  result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
-  case "$result" in
-    sat) echo "SZS Satisfiable for $filename"; exit 0;;
-    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
-    conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
-    conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
-  esac
+    sat) echo "% SZS Satisfiable for $filename";
+         echo "% SZS output start FiniteModel for $filename";
+         cat;
+         echo "% SZS output end FiniteModel for $filename";
+         exit 0;;
+    unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS CounterSatisfiable for $filename";
+                    echo "% SZS output start FiniteModel for $filename";
+                    cat;
+                    echo "% SZS output end FiniteModel for $filename";
+                    exit 0;;
+    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
 
 trywith 30 --finite-model-find --uf-ss-totality
 trywith 30 --finite-model-find --decision=justification --fmf-fmc
 trywith $to --finite-model-find --decision=justification
-echo "SZS GaveUp for $filename"
\ No newline at end of file
+echo "% SZS GaveUp for $filename"
\ No newline at end of file
diff --git a/contrib/run-script-casc24-fnt-no-models b/contrib/run-script-casc24-fnt-no-models
new file mode 100755
index 000000000..a189c10bd
--- /dev/null
+++ b/contrib/run-script-casc24-fnt-no-models
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+let "to = $2 - 60"
+
+file=${bench##*/}
+filename=${file%.*}
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
+# which case this run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "% SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
+  esac
+}
+function finishwith {
+  result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "% SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
+  esac
+}
+
+trywith 30 --finite-model-find --uf-ss-totality
+trywith 30 --finite-model-find --decision=justification --fmf-fmc
+trywith $to --finite-model-find --decision=justification
+echo "% SZS GaveUp for $filename"
\ No newline at end of file
diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof
index eb8e91310..940e26946 100755
--- a/contrib/run-script-casc24-fof
+++ b/contrib/run-script-casc24-fof
@@ -14,19 +14,19 @@ filename=${file%.*}
 function trywith {
   result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
   case "$result" in
-    sat) echo "SZS Satisfiable for $filename"; exit 0;;
-    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
-    conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
-    conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
+    sat) echo "% SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
   esac
 }
 function finishwith {
   result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
   case "$result" in
-    sat) echo "SZS Satisfiable for $filename"; exit 0;;
-    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
-    conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
-    conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
+    sat) echo "% SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
   esac
 }
 
@@ -34,4 +34,4 @@ trywith 30
 trywith 15 --finite-model-find --fmf-inst-engine
 trywith 30 --finite-model-find --decision=justification --fmf-fmc
 trywith $to --decision=justification
-echo "SZS GaveUp for $filename"
\ No newline at end of file
+echo "% SZS GaveUp for $filename"
\ No newline at end of file
diff --git a/library_versions b/library_versions
index eac360c34..ad37ce67a 100644
--- a/library_versions
+++ b/library_versions
@@ -53,3 +53,5 @@
 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?
+# note: removed Parser::getDeclarationLevel(), added other interfaces
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 0ecc6b5c7..601c251d9 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2273,7 +2273,7 @@ void ValidityChecker::popto(int stackLevel) {
 }
 
 int ValidityChecker::scopeLevel() {
-  return d_parserContext->getDeclarationLevel();
+  return d_parserContext->scopeLevel();
 }
 
 void ValidityChecker::pushScope() {
@@ -2287,12 +2287,12 @@ void ValidityChecker::popScope() {
 void ValidityChecker::poptoScope(int scopeLevel) {
   CVC4::CheckArgument(scopeLevel >= 0, scopeLevel,
                       "Cannot pop to a negative scope level %d", scopeLevel);
-  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(),
+  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
                       scopeLevel,
                       "Cannot pop to a scope level higher than the current one!  "
                       "At scope level %u, user requested scope level %d",
-                      d_parserContext->getDeclarationLevel(), scopeLevel);
-  while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) {
+                      d_parserContext->scopeLevel(), scopeLevel);
+  while(unsigned(scopeLevel) < d_parserContext->scopeLevel()) {
     popScope();
   }
 }
diff --git a/src/cvc4.i b/src/cvc4.i
index 965452b84..386bd00b5 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -54,9 +54,11 @@ using namespace CVC4;
 #include "expr/expr.h"
 #include "util/datatype.h"
 #include "expr/command.h"
-#include "bindings/java_stream_adapters.h"
 
+#ifdef SWIGJAVA
+#include "bindings/java_stream_adapters.h"
 std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
+#endif
 %}
 
 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 3a88a6cba..36336a959 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -795,17 +795,17 @@ const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
 
 void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<Node> result;
-    NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager());
+    vector<Expr> result;
+    ExprManager* em = smtEngine->getExprManager();
+    NodeManager* nm = NodeManager::fromExprManager(em);
     for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
       Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
       smt::SmtScope scope(smtEngine);
       Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
       Node value = Node::fromExpr(smtEngine->getValue(*i));
-      result.push_back(nm->mkNode(kind::SEXPR, request, value));
+      result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
     }
-    Node n = nm->mkNode(kind::SEXPR, result);
-    d_result = nm->toExpr(n);
+    d_result = em->mkExpr(kind::SEXPR, result);
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -1228,11 +1228,9 @@ std::string GetOptionCommand::getFlag() const throw() {
 
 void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<SExpr> v;
-    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
-    v.push_back(smtEngine->getOption(d_flag));
+    SExpr res = smtEngine->getOption(d_flag);
     stringstream ss;
-    ss << SExpr(v);
+    ss << res;
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(UnrecognizedOptionException&) {
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 977345a63..c649a5ebb 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -9,7 +9,11 @@
 #endif /* SWIGJAVA */
 %}
 
+#ifdef SWIGPYTHON
+%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
+#else /* SWIGPYTHON */
 %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
+#endif /* SWIGPYTHON */
 
 %ignore CVC4::operator<<(std::ostream&, const Expr&);
 %ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
diff --git a/src/expr/type.i b/src/expr/type.i
index e227cca23..6394dda67 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -2,7 +2,11 @@
 #include "expr/type.h"
 %}
 
+#ifdef SWIGPYTHON
+%rename(doApply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
+#else /* SWIGPYTHON */
 %rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
+#endif /* SWIGPYTHON */
 
 %ignore CVC4::operator<<(std::ostream&, const Type&);
 
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index f1742b549..556e51216 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -19,6 +19,8 @@
 
 #include "main/main.h"
 
+#include "smt/options.h"
+
 namespace CVC4 {
 namespace main {
 
@@ -64,6 +66,17 @@ bool CommandExecutor::doCommandSingleton(Command *cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
+  //dump the model if option is set
+  if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
+    CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
+    if(cs != NULL) {
+      if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
+         (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
+        Command * gm = new GetModelCommand;
+        status = doCommandSingleton(gm);
+      }
+    }
+  }
   return status;
 }
 
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 3376e9d0b..5c9f8af21 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -313,7 +313,11 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    d_out << pe << endl;
+    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+      d_out << "(error \"" << pe << "\")" << endl;
+    } else {
+      d_out << pe << endl;
+    }
     // We can't really clear out the sequence and abort the current line,
     // because the parse error might be for the second command on the
     // line.  The first ones haven't yet been executed by the SmtEngine,
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 7b61b48aa..a4c4b9c0a 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -37,10 +37,12 @@
 #include "util/output.h"
 #include "util/result.h"
 #include "util/statistics.h"
+#include "util/language.h"
 
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::main;
+using namespace CVC4::language;
 
 /**
  * CVC4's main() routine is just an exception-safe wrapper around CVC4.
@@ -64,7 +66,11 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts[options::out] << "unknown" << endl;
 #endif
-    *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+      *opts[options::err] << "(error \"" << e << "\")" << endl;
+    } else {
+      *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+    }
     if(opts[options::statistics] && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(*opts[options::err]);
diff --git a/src/options/mkoptions b/src/options/mkoptions
index fa6c4c260..2e152ee07 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -666,13 +666,40 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 
   if [ -n "$smtname" ]; then
     if [ "$internal" != - ]; then
-      smt_getoption_handlers="${smt_getoption_handlers}
+      case "$type" in
+      bool) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExprKeyword(options::$internal() ? \"true\" : \"false\");
+  }";;
+      int|unsigned|int*_t|uint*_t|CVC4::Integer) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExpr(Integer(options::$internal()));
+  }";;
+      float|double) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    stringstream ss; ss << std::fixed << options::$internal();
+    return SExpr(Rational::fromDecimal(ss.str()));
+  }";;
+      CVC4::Rational) smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExpr(options::$internal());
+  }";;
+      *) smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     stringstream ss; ss << options::$internal();
     return SExpr(ss.str());
-  }"
+  }";;
+      esac
     fi
 
     if [ "$type" = bool ]; then
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 217e7ab97..cf21ca6eb 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1184,7 +1184,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
 
     /* bitvector types */
   | BITVECTOR_TOK LPAREN k=numeral RPAREN
-    { t = EXPR_MANAGER->mkBitVectorType(k); }
+    { if(k == 0) {
+        PARSER_STATE->parseError("Illegal bitvector size: 0");
+      }
+      t = EXPR_MANAGER->mkBitVectorType(k);
+    }
 
     /* basic types */
   | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
@@ -1368,7 +1372,7 @@ letDecl
   : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
     { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
       PARSER_STATE->defineVar(name, e);
-      Debug("parser") << "LET[" << PARSER_STATE->getDeclarationLevel() << "]: "
+      Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
                       << name << std::endl
                       << " ==>" << " " << e << std::endl;
     }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 198d1cc31..370bdfcf0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -42,6 +42,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
   d_input(input),
   d_symtabAllocated(),
   d_symtab(&d_symtabAllocated),
+  d_assertionLevel(0),
   d_anonymousFunctionCount(0),
   d_done(false),
   d_checksEnabled(true),
@@ -357,7 +358,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return d_symtab->isBound(name);
+    return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name);
   case SYM_SORT:
     return d_symtab->isBoundType(name);
   }
@@ -365,6 +366,11 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) {
   return false;
 }
 
+void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
+  checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE);
+  d_reservedSymbols.insert(varName);
+}
+
 void Parser::checkDeclaration(const std::string& varName,
                               DeclarationCheck check,
                               SymbolType type)
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1ca56dc06..4f943a0b5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -126,6 +126,23 @@ class CVC4_PUBLIC Parser {
    */
   SymbolTable* d_symtab;
 
+  /**
+   * The level of the assertions in the declaration scope.  Things declared
+   * after this level are bindings from e.g. a let, a quantifier, or a
+   * lambda.
+   */
+  size_t d_assertionLevel;
+
+  /**
+   * Maintains a list of reserved symbols at the assertion level that might
+   * not occur in our symbol table.  This is necessary to e.g. support the
+   * proper behavior of the :named annotation in SMT-LIBv2 when used under
+   * a let or a quantifier, since inside a let/quant body the declaration
+   * scope is that of the let/quant body, but the defined name should be
+   * reserved at the assertion level.
+   */
+  std::set<std::string> d_reservedSymbols;
+
   /** How many anonymous functions we've created. */
   size_t d_anonymousFunctionCount;
 
@@ -288,6 +305,11 @@ public:
                         SymbolType type = SYM_VARIABLE) throw(ParserException);
 
   /**
+   * Reserve a symbol at the assertion level.
+   */
+  void reserveSymbolAtAssertionLevel(const std::string& name);
+
+  /**
    * Checks whether the given name is bound to a function.
    * @param name the name to check
    * @throws ParserException if checks are enabled and name is not
@@ -462,6 +484,11 @@ public:
     d_input->parseError(msg);
   }
 
+  /** Unexpectedly encountered an EOF */
+  inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
+    d_input->parseError(msg, true);
+  }
+
   /**
    * If we are parsing only, don't raise an exception; if we are not,
    * raise a parse error with the given message.  There is no actual
@@ -482,8 +509,25 @@ public:
     }
   }
 
-  inline void pushScope() { d_symtab->pushScope(); }
-  inline void popScope() { d_symtab->popScope(); }
+  /**
+   * Gets the current declaration level.
+   */
+  inline size_t scopeLevel() const { return d_symtab->getLevel(); }
+
+  inline void pushScope(bool bindingLevel = false) {
+    d_symtab->pushScope();
+    if(!bindingLevel) {
+      d_assertionLevel = scopeLevel();
+    }
+  }
+
+  inline void popScope() {
+    d_symtab->popScope();
+    if(scopeLevel() < d_assertionLevel) {
+      d_assertionLevel = scopeLevel();
+      d_reservedSymbols.clear();
+    }
+  }
 
   /**
    * Set the current symbol table used by this parser.
@@ -527,13 +571,6 @@ public:
   }
 
   /**
-   * Gets the current declaration level.
-   */
-  inline size_t getDeclarationLevel() const throw() {
-    return d_symtab->getLevel();
-  }
-
-  /**
    * An expression stream interface for a parser.  This stream simply
    * pulls expressions from the given Parser object.
    *
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8dcde2483..133cedfbd 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -133,6 +133,41 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
+static bool isClosed(Expr e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
+  if(closedCache.find(e) != closedCache.end()) {
+    return true;
+  }
+
+  if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) {
+    isClosed(e[1], free, closedCache);
+    for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) {
+      free.erase((*i)[0]);
+    }
+  } else if(e.getKind() == kind::BOUND_VARIABLE) {
+    free.insert(e);
+    return false;
+  } else {
+    if(e.hasOperator()) {
+      isClosed(e.getOperator(), free, closedCache);
+    }
+    for(Expr::const_iterator i = e.begin(); i != e.end(); ++i) {
+      isClosed(*i, free, closedCache);
+    }
+  }
+
+  if(free.empty()) {
+    closedCache.insert(e);
+    return true;
+  } else {
+    return false;
+  }
+}
+
+static inline bool isClosed(Expr e, std::set<Expr>& free) {
+  std::hash_set<Expr, ExprHashFunction> cache;
+  return isClosed(e, free, cache);
+}
+
 }/* parser::postinclude */
 
 /**
@@ -216,7 +251,7 @@ command returns [CVC4::Command* cmd = NULL]
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
-    { PARSER_STATE->pushScope();
+    { PARSER_STATE->pushScope(true);
       for(std::vector<std::string>::const_iterator i = names.begin(),
             iend = names.end();
           i != iend;
@@ -262,7 +297,7 @@ command returns [CVC4::Command* cmd = NULL]
         }
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -284,7 +319,7 @@ command returns [CVC4::Command* cmd = NULL]
     { $cmd = new GetValueCommand(terms); }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetAssignmentCommand; }
+    { cmd = new GetAssignmentCommand(); }
   | /* assertion */
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[expr, expr2]
@@ -294,13 +329,13 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
   | /* get-assertions */
     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetAssertionsCommand; }
+    { cmd = new GetAssertionsCommand(); }
   | /* get-proof */
     GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetProofCommand; }
+    { cmd = new GetProofCommand(); }
   | /* get-unsat-core */
     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetUnsatCoreCommand; }
+    { cmd = new GetUnsatCoreCommand(); }
   | /* push */
     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
@@ -314,7 +349,9 @@ command returns [CVC4::Command* cmd = NULL]
           CommandSequence* seq = new CommandSequence();
           do {
             PARSER_STATE->pushScope();
-            seq->addCommand(new PushCommand());
+            Command* c = new PushCommand();
+            c->setMuted(n > 1);
+            seq->addCommand(c);
           } while(--n > 0);
           cmd = seq;
         }
@@ -322,12 +359,15 @@ command returns [CVC4::Command* cmd = NULL]
     | { if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
         } else {
-          cmd = new PushCommand;
+          cmd = new PushCommand();
         }
       } )
   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
       { unsigned n = AntlrInput::tokenToUnsigned(k);
+        if(n > PARSER_STATE->scopeLevel()) {
+          PARSER_STATE->parseError("Attempted to pop above the top stack frame.");
+        }
         if(n == 0) {
           cmd = new EmptyCommand();
         } else if(n == 1) {
@@ -337,7 +377,9 @@ command returns [CVC4::Command* cmd = NULL]
           CommandSequence* seq = new CommandSequence();
           do {
             PARSER_STATE->popScope();
-            seq->addCommand(new PopCommand());
+            Command* c = new PopCommand();
+            c->setMuted(n > 1);
+            seq->addCommand(c);
           } while(--n > 0);
           cmd = seq;
         }
@@ -345,11 +387,11 @@ command returns [CVC4::Command* cmd = NULL]
     | { if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
         } else {
-          cmd = new PopCommand;
+          cmd = new PopCommand();
         }
       } )
   | EXIT_TOK
-    { cmd = new QuitCommand; }
+    { cmd = new QuitCommand(); }
 
     /* CVC4-extended SMT-LIB commands */
   | extendedCommand[cmd]
@@ -385,7 +427,7 @@ extendedCommand[CVC4::Command*& cmd]
      * --smtlib2 compliance mode. */
   : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { /* open a scope to keep the UnresolvedTypes contained */
-      PARSER_STATE->pushScope(); }
+      PARSER_STATE->pushScope(true); }
     LPAREN_TOK 	/* parametric sorts */
       ( symbol[name,CHECK_UNDECLARED,SYM_SORT] {
         sorts.push_back( PARSER_STATE->mkSort(name) ); }
@@ -396,7 +438,7 @@ extendedCommand[CVC4::Command*& cmd]
       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
   | /* get model */
     GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetModelCommand; }
+    { cmd = new GetModelCommand(); }
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
       { std::stringstream ss;
@@ -474,7 +516,7 @@ extendedCommand[CVC4::Command*& cmd]
       sortedVarList[sortedVarNames] RPAREN_TOK
       { /* add variables to parser state before parsing term */
         Debug("parser") << "define fun: '" << name << "'" << std::endl;
-        PARSER_STATE->pushScope();
+        PARSER_STATE->pushScope(true);
         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
               sortedVarNames.begin(), iend = sortedVarNames.end();
             i != iend;
@@ -521,7 +563,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
       kind = CVC4::kind::RR_REWRITE;
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -562,7 +604,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
   | rewritePropaKind[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -704,13 +746,27 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       } else if( CVC4::kind::isAssociative(kind) &&
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
-        expr = EXPR_MANAGER->mkAssociative(kind,args);
+        expr = EXPR_MANAGER->mkAssociative(kind, args);
       } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
+      } else if( ( kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS ) &&
+                 args.size() > 2 ) {
+        /* left-associative, but CVC4 internally only supports 2 args */
+        expr = args[0];
+        for(size_t i = 1; i < args.size(); ++i) {
+          expr = MK_EXPR(kind, expr, args[i]);
+        }
+      } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) {
+        /* right-associative, but CVC4 internally only supports 2 args */
+        expr = args[args.size() - 1];
+        for(size_t i = args.size() - 1; i > 0;) {
+          expr = MK_EXPR(kind, args[--i], expr);
+        }
       } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL ||
                    kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
                    kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
                  args.size() > 2 ) {
+        /* "chainable", but CVC4 internally only supports 2 args */
         expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args);
       } else {
         PARSER_STATE->checkOperator(kind, args.size());
@@ -736,7 +792,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | LPAREN_TOK quantOp[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -805,7 +861,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
-    { PARSER_STATE->pushScope(); }
+    { PARSER_STATE->pushScope(true); }
     ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
       // this is a parallel let, so we have to save up all the contributions
       // of the let and define them only later on
@@ -971,10 +1027,24 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
+      if(!sexpr.isKeyword()) {
+        PARSER_STATE->parseError("improperly formed :named annotation");
+      }
       std::string name = sexpr.getValue();
-      // FIXME ensure expr is a closed subterm
-      // check that sexpr is a fresh function symbol
-      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      PARSER_STATE->checkUserSymbol(name);
+      // ensure expr is a closed subterm
+      std::set<Expr> freeVars;
+      if(!isClosed(expr, freeVars)) {
+        assert(!freeVars.empty());
+        std::stringstream ss;
+        ss << ":named annotations can only name terms that are closed; this one contains free variables:";
+        for(std::set<Expr>::const_iterator i = freeVars.begin(); i != freeVars.end(); ++i) {
+          ss << " " << *i;
+        }
+        PARSER_STATE->parseError(ss.str());
+      }
+      // check that sexpr is a fresh function symbol, and reserve it
+      PARSER_STATE->reserveSymbolAtAssertionLevel(name);
       // define it
       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
       // bind name to expr with define-fun
@@ -1200,6 +1270,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
         if( numerals.size() != 1 ) {
           PARSER_STATE->parseError("Illegal bitvector type.");
         }
+        if(numerals.front() == 0) {
+          PARSER_STATE->parseError("Illegal bitvector size: 0");
+        }
         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
       } else {
         std::stringstream ss;
@@ -1271,6 +1344,8 @@ symbol[std::string& id,
         PARSER_STATE->checkDeclaration(id, check, type);
       }
     }
+  | UNTERMINATED_QUOTED_SYMBOL EOF
+    { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
   ;
 
 /**
@@ -1294,7 +1369,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& p
      * datatypes won't work, because this type will already be
      * "defined" as an unresolved type; don't worry, we check
      * below. */
-  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
+  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
    /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
         t = PARSER_STATE->mkSort(id2);
         params.push_back( t );
@@ -1464,6 +1539,9 @@ BVSGE_TOK : 'bvsge';
 QUOTED_SYMBOL
   : '|' ~('|' | '\\')* '|'
   ;
+UNTERMINATED_QUOTED_SYMBOL
+  : '|' ~('|' | '\\')*
+  ;
 
 /**
  * Matches a keyword from the input. A keyword is a simple symbol prefixed
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 0063035ff..166a695a4 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -715,7 +715,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         // push children
         for(int i = top.getNumChildren() - 1; i >= 0; --i) {
           Debug("bt") << "rewriting: " << top[i] << endl;
-          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), false));
+          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : (isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
           //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
           //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
         }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e49e6fb54..ca89ce36d 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 {
@@ -823,15 +823,6 @@ void SmtEngine::setLogicInternal() throw() {
 
   d_logic.lock();
 
-  // may need to force uninterpreted functions to be on for non-linear
-  if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ||
-      d_logic.isTheoryEnabled(THEORY_BV)) &&
-     !d_logic.isTheoryEnabled(THEORY_UF)){
-    d_logic = d_logic.getUnlockedCopy();
-    d_logic.enableTheory(THEORY_UF);
-    d_logic.lock();
-  }
-
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
@@ -1322,6 +1313,11 @@ Node SmtEnginePrivate::expandBVDivByZero(TNode n) {
   Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
                                    kind::BITVECTOR_UREM_TOTAL, num, den);
   Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+  if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+    d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+    d_smt.d_logic.enableTheory(THEORY_UF);
+    d_smt.d_logic.lock();
+  }
   return node;
 }
 
@@ -1372,13 +1368,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   }
   case kind::DIVISION: {
     // partial function: division
-    if(d_smt.d_logic.isLinear()) {
-      node = n;
-      break;
-    }
     if(d_divByZero.isNull()) {
       d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()),
                                  "partial real division", NodeManager::SKOLEM_EXACT_NAME);
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_UF);
+        d_smt.d_logic.lock();
+      }
     }
     TNode num = n[0], den = n[1];
     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
@@ -1390,13 +1387,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
   case kind::INTS_DIVISION: {
     // partial function: integer div
-    if(d_smt.d_logic.isLinear()) {
-      node = n;
-      break;
-    }
     if(d_intDivByZero.isNull()) {
       d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
                                     "partial integer division", NodeManager::SKOLEM_EXACT_NAME);
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_UF);
+        d_smt.d_logic.lock();
+      }
     }
     TNode num = n[0], den = n[1];
     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
@@ -1408,13 +1406,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
   case kind::INTS_MODULUS: {
     // partial function: mod
-    if(d_smt.d_logic.isLinear()) {
-      node = n;
-      break;
-    }
     if(d_modZero.isNull()) {
       d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
                                "partial modulus", NodeManager::SKOLEM_EXACT_NAME);
+      if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+        d_smt.d_logic.enableTheory(THEORY_UF);
+        d_smt.d_logic.lock();
+      }
     }
     TNode num = n[0], den = n[1];
     Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
@@ -3327,7 +3326,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
   }
 
   if(d_assignments == NULL) {
-    return SExpr();
+    return SExpr(vector<SExpr>());
   }
 
   vector<SExpr> sexprs;
@@ -3639,6 +3638,11 @@ void SmtEngine::push() throw(ModalException, LogicException) {
     d_needPostsolve = false;
   }
 
+  // The problem isn't really "extended" yet, but this disallows
+  // get-model after a push, simplifying our lives somewhat and
+  // staying symmtric with pop.
+  d_problemExtended = true;
+
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
   Trace("userpushpop") << "SmtEngine: pushed to level "
@@ -3665,6 +3669,14 @@ void SmtEngine::pop() throw(ModalException) {
     d_needPostsolve = false;
   }
 
+  // The problem isn't really "extended" yet, but this disallows
+  // get-model after a pop, simplifying our lives somewhat.  It might
+  // not be strictly necessary to do so, since the pops occur lazily,
+  // but also it would be weird to have a legally-executed (get-model)
+  // that only returns a subset of the assignment (because the rest
+  // is no longer in scope!).
+  d_problemExtended = true;
+
   AlwaysAssert(d_userContext->getLevel() > 0);
   AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a22e34c21..1b5af415f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine {
   bool d_fullyInited;
 
   /**
-   * Whether or not we have added any assertions/declarations/definitions
-   * since the last checkSat/query (and therefore we're not responsible
-   * for an assignment).
+   * Whether or not we have added any assertions/declarations/definitions,
+   * or done push/pop, since the last checkSat/query, and therefore we're
+   * not responsible for models or proofs.
    */
   bool d_problemExtended;
 
@@ -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/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 <glpk.h>
-}
+/* Sometimes the header is in a subdirectory glpk/, sometimes not.
+ * The configure script figures it out. */
+#ifdef HAVE_GLPK_GLPK_H
+#  include <glpk/glpk.h>
+#else /* HAVE_GLPK_GLPK_H */
+#  include <glpk.h>
+#endif /* HAVE_GLPK_GLPK_H */
+}/* extern "C" */
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3b141bf9e..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( d_quantEngine && d_quantEngine->getBoundedIntegers() ){
+  if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){
     d_quantEngine->getBoundedIntegers()->assertNode(assertion);
   }
 
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());
   }
 
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<Node>::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/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<Node>::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<Node>& 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<Node> d_assertionsToRerun;
+  bool d_rerunningAssertions;
+
   std::vector<Node> d_phi;
   std::set<TNode> 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<Node>& 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/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<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
     std::vector<Node> 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/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 12d7ab397..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
@@ -42,6 +42,7 @@ SMT_TESTS = \
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = \
+	chained-equality.smt2 \
 	ite2.smt2 \
 	ite3.smt2 \
 	ite4.smt2 \
@@ -114,6 +115,7 @@ TPTP_TESTS = \
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
+	GEO123+1.minimized.smt2 \
 	smt2output.smt2 \
 	bug32.cvc \
 	bug49.smt \
@@ -149,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)
diff --git a/test/regress/regress0/chained-equality.smt2 b/test/regress/regress0/chained-equality.smt2
new file mode 100644
index 000000000..fb3a25b94
--- /dev/null
+++ b/test/regress/regress0/chained-equality.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-info :status unsat)
+(set-logic QF_UF)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+(assert (= x y z))
+(assert (not x))
+(assert z)
+(check-sat)
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)