Remove quantifiers rewrite rules infrastructure (#3754)

56 files changed, 25 insertions, 3874 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 975dd26f6..871cb2f99 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -544,8 +544,6 @@ libcvc4_add_sources(
   theory/quantifiers/query_generator.h
   theory/quantifiers/relevant_domain.cpp
   theory/quantifiers/relevant_domain.h
-  theory/quantifiers/rewrite_engine.cpp
-  theory/quantifiers/rewrite_engine.h
   theory/quantifiers/single_inv_partition.cpp
   theory/quantifiers/single_inv_partition.h
   theory/quantifiers/skolemize.cpp
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index bb2700706..2242c8e00 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2181,14 +2181,6 @@ enum CVC4_PUBLIC Kind : int32_t
   INST_PATTERN_LIST,
   /* predicate for specifying term in instantiation closure. */
   INST_CLOSURE,
-  /* general rewrite rule (for rewrite-rules theory) */
-  REWRITE_RULE,
-  /* actual rewrite rule (for rewrite-rules theory) */
-  RR_REWRITE,
-  /* actual reduction rule (for rewrite-rules theory) */
-  RR_REDUCTION,
-  /* actual deduction rule (for rewrite-rules theory) */
-  RR_DEDUCTION,
 
   /* Sort Kinds ------------------------------------------------------------ */
 
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 3cd6a7e51..7c2985e5c 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -160,7 +160,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/PopCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java
   ${CMAKE_CURRENT_BINARY_DIR}/Proof.java
-  ${CMAKE_CURRENT_BINARY_DIR}/PropagateRuleCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/PushCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/QueryCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/QuitCommand.java
@@ -177,7 +176,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/ResetCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/ResourceManager.java
   ${CMAKE_CURRENT_BINARY_DIR}/Result.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RewriteRuleCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 908846bea..84545e66e 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -899,15 +899,6 @@ header = "options/quantifiers_options.h"
 ### Rewrite rules options
 
 [[option]]
-  name       = "quantRewriteRules"
-  category   = "regular"
-  long       = "rewrite-rules"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "use rewrite rules module"
-
-[[option]]
   name       = "rrOneInstPerRound"
   category   = "regular"
   long       = "rr-one-inst-per-round"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index aed62f94c..90303dd40 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1254,8 +1254,6 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
   | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
   | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
   | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
-  | rewriterulesCommand[cmd]
-
     /* Support some of Z3's extended SMT-LIB commands */
 
   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1545,43 +1543,6 @@ datatypesDef[bool isCo,
   }
   ;
 
-rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd]
-@declarations {
-  std::vector<Expr> guards, heads, triggers;
-  Expr head, body, bvl, expr, expr2;
-  Kind kind;
-}
-  : /* rewrite rules */
-    REWRITE_RULE_TOK { kind = CVC4::kind::RR_REWRITE; }
-    { PARSER_STATE->pushScope(true); }
-    boundVarList[bvl]
-    LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
-    LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
-    term[head, expr2]
-    term[body, expr2]
-    {
-      *cmd = PARSER_STATE->assertRewriteRule(
-          kind, bvl, triggers, guards, {head}, body);
-    }
-    /* propagation rule */
-  | rewritePropaKind[kind]
-    { PARSER_STATE->pushScope(true); }
-    boundVarList[bvl]
-    LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK
-    LPAREN_TOK (termList[guards,expr])? RPAREN_TOK
-    LPAREN_TOK (termList[heads,expr])? RPAREN_TOK
-    term[body, expr2]
-    {
-      *cmd = PARSER_STATE->assertRewriteRule(
-          kind, bvl, triggers, guards, heads, body);
-    }
-  ;
-
-rewritePropaKind[CVC4::Kind& kind]
-  : REDUCTION_RULE_TOK    { $kind = CVC4::kind::RR_REDUCTION; }
-  | PROPAGATION_RULE_TOK  { $kind = CVC4::kind::RR_DEDUCTION; }
-  ;
-
 pattern[CVC4::Expr& expr]
 @declarations {
   std::vector<Expr> patexpr;
@@ -1631,8 +1592,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
         | GET_UNSAT_CORE_TOK | EXIT_TOK
         | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
         | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
-        | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK
-        | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
+        | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
   ;
 
@@ -1713,25 +1673,11 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       args.push_back(bvl);
 
       PARSER_STATE->popScope();
-      switch(f.getKind()) {
-      case CVC4::kind::RR_REWRITE:
-      case CVC4::kind::RR_REDUCTION:
-      case CVC4::kind::RR_DEDUCTION:
-        if(kind == CVC4::kind::EXISTS) {
-          PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite "
-                                   "rule.");
-        }
-        args.push_back(f2); // guards
-        args.push_back(f); // rule
-        expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
-        break;
-      default:
-        args.push_back(f);
-        if(! f2.isNull()){
-          args.push_back(f2);
-        }
-        expr = MK_EXPR(kind, args);
+      args.push_back(f);
+      if(! f2.isNull()){
+        args.push_back(f2);
       }
+      expr = MK_EXPR(kind, args);
     }
   | LPAREN_TOK COMPREHENSION_TOK
     { PARSER_STATE->pushScope(true); }
@@ -1902,33 +1848,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       }
     )+ RPAREN_TOK
     {
-      if(attr == ":rewrite-rule") {
-        Expr guard;
-        Expr body;
-        if(expr[1].getKind() == kind::IMPLIES ||
-           expr[1].getKind() == kind::EQUAL) {
-          guard = expr[0];
-          body = expr[1];
-        } else {
-          guard = MK_CONST(bool(true));
-          body = expr;
-        }
-        expr2 = guard;
-        args.push_back(body[0]);
-        args.push_back(body[1]);
-        if(!f2.isNull()) {
-          args.push_back(f2);
-        }
-
-        if( body.getKind()==kind::IMPLIES ){
-          kind = kind::RR_DEDUCTION;
-        }else if( body.getKind()==kind::EQUAL ){
-          kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE;
-        }else{
-          PARSER_STATE->parseError("Error parsing rewrite rule.");
-        }
-        expr = MK_EXPR( kind, args );
-      } else if(! patexprs.empty()) {
+      if(! patexprs.empty()) {
         if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
           for( size_t i=0; i<f2.getNumChildren(); i++ ){
             if( f2[i].getKind()==kind::INST_PATTERN ){
@@ -2702,9 +2622,6 @@ GET_MODEL_TOK : 'get-model';
 BLOCK_MODEL_TOK : 'block-model';
 BLOCK_MODEL_VALUES_TOK : 'block-model-values';
 ECHO_TOK : 'echo';
-REWRITE_RULE_TOK : 'assert-rewrite';
-REDUCTION_RULE_TOK : 'assert-reduction';
-PROPAGATION_RULE_TOK : 'assert-propagation';
 DECLARE_SORTS_TOK : 'declare-sorts';
 DECLARE_FUNS_TOK : 'declare-funs';
 DECLARE_PREDS_TOK : 'declare-preds';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3ab3c0eb1..9800cbe91 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -626,33 +626,6 @@ void Smt2::resetAssertions() {
   }
 }
 
-std::unique_ptr<Command> Smt2::assertRewriteRule(
-    Kind kind,
-    Expr bvl,
-    const std::vector<Expr>& triggers,
-    const std::vector<Expr>& guards,
-    const std::vector<Expr>& heads,
-    Expr body)
-{
-  assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION
-         || kind == kind::RR_DEDUCTION);
-
-  ExprManager* em = getExprManager();
-
-  std::vector<Expr> args;
-  args.push_back(mkAnd(heads));
-  args.push_back(body);
-
-  if (!triggers.empty())
-  {
-    args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers));
-  }
-
-  Expr rhs = em->mkExpr(kind, args);
-  Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs);
-  return std::unique_ptr<Command>(new AssertCommand(rule, false));
-}
-
 Smt2::SynthFunFactory::SynthFunFactory(
     Smt2* smt2,
     const std::string& fun,
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 6c1275115..6427b32d5 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -198,24 +198,6 @@ class Smt2 : public Parser
   void resetAssertions();
 
   /**
-   * Creates a command that asserts a rule.
-   *
-   * @param kind The kind of rule (RR_REWRITE, RR_REDUCTION, RR_DEDUCTION)
-   * @param bvl Bound variable list
-   * @param triggers List of triggers
-   * @param guards List of guards
-   * @param heads List of heads
-   * @param body The body of the rule
-   * @return The command that asserts the rewrite rule
-   */
-  std::unique_ptr<Command> assertRewriteRule(Kind kind,
-                                             Expr bvl,
-                                             const std::vector<Expr>& triggers,
-                                             const std::vector<Expr>& guards,
-                                             const std::vector<Expr>& heads,
-                                             Expr body);
-
-  /**
    * Class for creating instances of `SynthFunCommand`s. Creating an instance
    * of this class pushes the scope, destroying it pops the scope.
    */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 17d8cbed5..ce8d4fa88 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2841,251 +2841,4 @@ std::string DatatypeDeclarationCommand::getCommandName() const
   return "declare-datatypes";
 }
 
-/* -------------------------------------------------------------------------- */
-/* class RewriteRuleCommand                                                   */
-/* -------------------------------------------------------------------------- */
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
-                                       const std::vector<Expr>& guards,
-                                       Expr head,
-                                       Expr body,
-                                       const Triggers& triggers)
-    : d_vars(vars),
-      d_guards(guards),
-      d_head(head),
-      d_body(body),
-      d_triggers(triggers)
-{
-}
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
-                                       Expr head,
-                                       Expr body)
-    : d_vars(vars), d_head(head), d_body(body)
-{
-}
-
-const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; }
-const std::vector<Expr>& RewriteRuleCommand::getGuards() const
-{
-  return d_guards;
-}
-
-Expr RewriteRuleCommand::getHead() const { return d_head; }
-Expr RewriteRuleCommand::getBody() const { return d_body; }
-const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const
-{
-  return d_triggers;
-}
-
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine)
-{
-  try
-  {
-    ExprManager* em = smtEngine->getExprManager();
-    /** build vars list */
-    Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
-    /** build guards list */
-    Expr guards;
-    if (d_guards.size() == 0)
-      guards = em->mkConst<bool>(true);
-    else if (d_guards.size() == 1)
-      guards = d_guards[0];
-    else
-      guards = em->mkExpr(kind::AND, d_guards);
-    /** build expression */
-    Expr expr;
-    if (d_triggers.empty())
-    {
-      expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body);
-    }
-    else
-    {
-      /** build triggers list */
-      std::vector<Expr> vtriggers;
-      vtriggers.reserve(d_triggers.size());
-      for (Triggers::const_iterator i = d_triggers.begin(),
-                                    end = d_triggers.end();
-           i != end;
-           ++i)
-      {
-        vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
-      }
-      Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
-      expr =
-          em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers);
-    }
-    smtEngine->assertFormula(expr);
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* RewriteRuleCommand::exportTo(ExprManager* exprManager,
-                                      ExprManagerMapCollection& variableMap)
-{
-  /** Convert variables */
-  VExpr vars = ExportTo(exprManager, variableMap, d_vars);
-  /** Convert guards */
-  VExpr guards = ExportTo(exprManager, variableMap, d_guards);
-  /** Convert triggers */
-  Triggers triggers;
-  triggers.reserve(d_triggers.size());
-  for (const std::vector<Expr>& trigger_list : d_triggers)
-  {
-    triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
-  }
-  /** Convert head and body */
-  Expr head = d_head.exportTo(exprManager, variableMap);
-  Expr body = d_body.exportTo(exprManager, variableMap);
-  /** Create the converted rules */
-  return new RewriteRuleCommand(vars, guards, head, body, triggers);
-}
-
-Command* RewriteRuleCommand::clone() const
-{
-  return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
-}
-
-std::string RewriteRuleCommand::getCommandName() const
-{
-  return "rewrite-rule";
-}
-
-/* -------------------------------------------------------------------------- */
-/* class PropagateRuleCommand                                                 */
-/* -------------------------------------------------------------------------- */
-
-PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
-                                           const std::vector<Expr>& guards,
-                                           const std::vector<Expr>& heads,
-                                           Expr body,
-                                           const Triggers& triggers,
-                                           bool deduction)
-    : d_vars(vars),
-      d_guards(guards),
-      d_heads(heads),
-      d_body(body),
-      d_triggers(triggers),
-      d_deduction(deduction)
-{
-}
-
-PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
-                                           const std::vector<Expr>& heads,
-                                           Expr body,
-                                           bool deduction)
-    : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction)
-{
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getVars() const
-{
-  return d_vars;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getGuards() const
-{
-  return d_guards;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getHeads() const
-{
-  return d_heads;
-}
-
-Expr PropagateRuleCommand::getBody() const { return d_body; }
-const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const
-{
-  return d_triggers;
-}
-
-bool PropagateRuleCommand::isDeduction() const { return d_deduction; }
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine)
-{
-  try
-  {
-    ExprManager* em = smtEngine->getExprManager();
-    /** build vars list */
-    Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
-    /** build guards list */
-    Expr guards;
-    if (d_guards.size() == 0)
-      guards = em->mkConst<bool>(true);
-    else if (d_guards.size() == 1)
-      guards = d_guards[0];
-    else
-      guards = em->mkExpr(kind::AND, d_guards);
-    /** build heads list */
-    Expr heads;
-    if (d_heads.size() == 1)
-      heads = d_heads[0];
-    else
-      heads = em->mkExpr(kind::AND, d_heads);
-    /** build expression */
-    Expr expr;
-    if (d_triggers.empty())
-    {
-      expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body);
-    }
-    else
-    {
-      /** build triggers list */
-      std::vector<Expr> vtriggers;
-      vtriggers.reserve(d_triggers.size());
-      for (Triggers::const_iterator i = d_triggers.begin(),
-                                    end = d_triggers.end();
-           i != end;
-           ++i)
-      {
-        vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
-      }
-      Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
-      expr =
-          em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers);
-    }
-    smtEngine->assertFormula(expr);
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* PropagateRuleCommand::exportTo(ExprManager* exprManager,
-                                        ExprManagerMapCollection& variableMap)
-{
-  /** Convert variables */
-  VExpr vars = ExportTo(exprManager, variableMap, d_vars);
-  /** Convert guards */
-  VExpr guards = ExportTo(exprManager, variableMap, d_guards);
-  /** Convert heads */
-  VExpr heads = ExportTo(exprManager, variableMap, d_heads);
-  /** Convert triggers */
-  Triggers triggers;
-  triggers.reserve(d_triggers.size());
-  for (const std::vector<Expr>& trigger_list : d_triggers)
-  {
-    triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
-  }
-  /** Convert head and body */
-  Expr body = d_body.exportTo(exprManager, variableMap);
-  /** Create the converted rules */
-  return new PropagateRuleCommand(vars, guards, heads, body, triggers);
-}
-
-Command* PropagateRuleCommand::clone() const
-{
-  return new PropagateRuleCommand(
-      d_vars, d_guards, d_heads, d_body, d_triggers);
-}
-
-std::string PropagateRuleCommand::getCommandName() const
-{
-  return "propagate-rule";
-}
 }  // namespace CVC4
diff --git a/src/smt/command.h b/src/smt/command.h
index d82399135..19b858bd6 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1315,80 +1315,6 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
   std::string getCommandName() const override;
 }; /* class DatatypeDeclarationCommand */
 
-class CVC4_PUBLIC RewriteRuleCommand : public Command
-{
- public:
-  typedef std::vector<std::vector<Expr> > Triggers;
-
- protected:
-  typedef std::vector<Expr> VExpr;
-  VExpr d_vars;
-  VExpr d_guards;
-  Expr d_head;
-  Expr d_body;
-  Triggers d_triggers;
-
- public:
-  RewriteRuleCommand(const std::vector<Expr>& vars,
-                     const std::vector<Expr>& guards,
-                     Expr head,
-                     Expr body,
-                     const Triggers& d_triggers);
-  RewriteRuleCommand(const std::vector<Expr>& vars, Expr head, Expr body);
-
-  const std::vector<Expr>& getVars() const;
-  const std::vector<Expr>& getGuards() const;
-  Expr getHead() const;
-  Expr getBody() const;
-  const Triggers& getTriggers() const;
-
-  void invoke(SmtEngine* smtEngine) override;
-  Command* exportTo(ExprManager* exprManager,
-                    ExprManagerMapCollection& variableMap) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-}; /* class RewriteRuleCommand */
-
-class CVC4_PUBLIC PropagateRuleCommand : public Command
-{
- public:
-  typedef std::vector<std::vector<Expr> > Triggers;
-
- protected:
-  typedef std::vector<Expr> VExpr;
-  VExpr d_vars;
-  VExpr d_guards;
-  VExpr d_heads;
-  Expr d_body;
-  Triggers d_triggers;
-  bool d_deduction;
-
- public:
-  PropagateRuleCommand(const std::vector<Expr>& vars,
-                       const std::vector<Expr>& guards,
-                       const std::vector<Expr>& heads,
-                       Expr body,
-                       const Triggers& d_triggers,
-                       /* true if we want a deduction rule */
-                       bool d_deduction = false);
-  PropagateRuleCommand(const std::vector<Expr>& vars,
-                       const std::vector<Expr>& heads,
-                       Expr body,
-                       bool d_deduction = false);
-
-  const std::vector<Expr>& getVars() const;
-  const std::vector<Expr>& getGuards() const;
-  const std::vector<Expr>& getHeads() const;
-  Expr getBody() const;
-  const Triggers& getTriggers() const;
-  bool isDeduction() const;
-  void invoke(SmtEngine* smtEngine) override;
-  Command* exportTo(ExprManager* exprManager,
-                    ExprManagerMapCollection& variableMap) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-}; /* class PropagateRuleCommand */
-
 class CVC4_PUBLIC ResetCommand : public Command
 {
  public:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ad4d4e1d5..1d96fc207 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3630,12 +3630,6 @@ void SmtEnginePrivate::addFormula(
       // n is the result of an unknown preprocessing step, add it to dependency map to null
       ProofManager::currentPM()->addDependence(n, Node::null());
     }
-    // rewrite rules are by default in the unsat core because
-    // they need to be applied until saturation
-    if(options::unsatCores() &&
-       n.getKind() == kind::REWRITE_RULE ){
-      ProofManager::currentPM()->addUnsatCore(n.toExpr());
-    }
   );
 
   // Add the normalized formula to the queue
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index dc11ed562..1534d2d4d 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -55,25 +55,4 @@ typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeType
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
 typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule 
 
-# for rewrite rules
-# types...
-sort RRHB_TYPE \
-    Cardinality::INTEGERS \
-    not-well-founded \
-    "head and body of the rule type (for rewrite-rules theory)"
-
-# operators...
-
-# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
-operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)"
-#HEAD/BODY/TRIGGER
-operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)"
-operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)"
-operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)"
-
-typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule
-typerule RR_REWRITE   ::CVC4::theory::quantifiers::RRRewriteTypeRule
-typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
-typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
-
 endtheory
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 0e6eb1581..af4011bd9 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -16,7 +16,6 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -80,12 +79,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
     QuantInstLevelAttribute qila;
     n.setAttribute( qila, lvl );
-  }else if( attr=="rr-priority" ){
-    Assert(node_values.size() == 1);
-    uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
-    Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
-    RrPriorityAttribute rrpa;
-    n.setAttribute( rrpa, lvl );
   }else if( attr=="quant-elim" ){
     Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
     QuantElimAttribute qea;
@@ -97,21 +90,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
   }
 }
 
-bool QuantAttributes::checkRewriteRule( Node q ) {
-  return !getRewriteRule( q ).isNull();
-}
-
-Node QuantAttributes::getRewriteRule( Node q ) {
-  if (q.getKind() == FORALL && q.getNumChildren() == 3
-      && q[2][0].getNumChildren() > 0
-      && q[2][0][0].getKind() == REWRITE_RULE)
-  {
-    return q[2][0][0];
-  }else{
-    return Node::null();
-  }
-}
-
 bool QuantAttributes::checkFunDef( Node q ) {
   return !getFunDefHead( q ).isNull();
 }
@@ -275,10 +253,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
           Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
         }
-        if( avar.hasAttribute(RrPriorityAttribute()) ){
-          qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
-          Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
-        }
         if( avar.getAttribute(QuantElimAttribute()) ){
           Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
           qa.d_quant_elim = true;
@@ -294,11 +268,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_qid_num = avar;
           Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
         }
-        if( avar.getKind()==REWRITE_RULE ){
-          Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
-          Assert(i == 0);
-          qa.d_rr = avar;
-        }
       }
     }
   }
@@ -349,15 +318,6 @@ int QuantAttributes::getQuantInstLevel( Node q ) {
   }
 }
 
-int QuantAttributes::getRewriteRulePriority( Node q ) {
-  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
-  if( it==d_qattr.end() ){
-    return -1;
-  }else{
-    return it->second.d_rr_priority;
-  }
-}
-
 bool QuantAttributes::isQuantElim( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 827c5e7f4..fc0f85956 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -111,7 +111,6 @@ struct QAttributes
         d_conjecture(false),
         d_axiom(false),
         d_sygus(false),
-        d_rr_priority(-1),
         d_qinstLevel(-1),
         d_quant_elim(false),
         d_quant_elim_partial(false)
@@ -120,9 +119,6 @@ struct QAttributes
   ~QAttributes(){}
   /** does the quantified formula have a pattern? */
   bool d_hasPattern;
-  /** if non-null, this is the rewrite rule representation of the quantified
-   * formula */
-  Node d_rr;
   /** is this formula marked a conjecture? */
   bool d_conjecture;
   /** is this formula marked an axiom? */
@@ -134,8 +130,6 @@ struct QAttributes
   bool d_sygus;
   /** side condition for sygus conjectures */
   Node d_sygusSideCondition;
-  /** if a rewrite rule, then this is the priority value for the rewrite rule */
-  int d_rr_priority;
   /** stores the maximum instantiation level allowed for this quantified formula
    * (-1 means allow any) */
   int d_qinstLevel;
@@ -150,8 +144,6 @@ struct QAttributes
   Node d_name;
   /** the quantifier id associated with this formula */
   Node d_qid_num;
-  /** is this quantified formula a rewrite rule? */
-  bool isRewriteRule() const { return !d_rr.isNull(); }
   /** is this quantified formula a function definition? */
   bool isFunDef() const { return !d_fundef_f.isNull(); }
   /**
@@ -193,10 +185,6 @@ public:
   /** compute the attributes for q */
   void computeAttributes(Node q);
 
-  /** is quantifier treated as a rewrite rule? */
-  static bool checkRewriteRule( Node q );
-  /** get the rewrite rule associated with the quanfied formula */
-  static Node getRewriteRule( Node q );
   /** is fun def */
   static bool checkFunDef( Node q );
   /** is fun def */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e35595287..e2ee99ceb 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -185,15 +185,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       //compute attributes
       QAttributes qa;
       QuantAttributes::computeQuantAttributes( in, qa );
-      if( !qa.isRewriteRule() ){
-        for( int op=0; op<COMPUTE_LAST; op++ ){
-          if( doOperation( in, op, qa ) ){
-            ret = computeOperation( in, op, qa );
-            if( ret!=in ){
-              rew_op = op;
-              status = REWRITE_AGAIN_FULL;
-              break;
-            }
+      for( int op=0; op<COMPUTE_LAST; op++ ){
+        if( doOperation( in, op, qa ) ){
+          ret = computeOperation( in, op, qa );
+          if( ret!=in ){
+            rew_op = op;
+            status = REWRITE_AGAIN_FULL;
+            break;
           }
         }
       }
@@ -2088,102 +2086,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }
 }
 
-
-Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
-  Kind rrkind = r[2].getKind();
-
-  //guards, pattern, body
-
-  //   Replace variables by Inst_* variable and tag the terms that contain them
-  std::vector<Node> vars;
-  vars.reserve(r[0].getNumChildren());
-  for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){
-    vars.push_back(*v);
-  };
-
-  // Body/Remove_term/Guards/Triggers
-  Node body = r[2][1];
-  TNode new_terms = r[2][1];
-  std::vector<Node> guards;
-  std::vector<Node> pattern;
-  Node true_node = NodeManager::currentNM()->mkConst(true);
-  // shortcut
-  TNode head = r[2][0];
-  switch(rrkind){
-  case kind::RR_REWRITE:
-    // Equality
-    pattern.push_back( head );
-    body = head.eqNode(body);
-    break;
-  case kind::RR_REDUCTION:
-  case kind::RR_DEDUCTION:
-    // Add head to guards and pattern
-    switch(head.getKind()){
-    case kind::AND:
-      for( unsigned i = 0; i<head.getNumChildren(); i++ ){
-        guards.push_back(head[i]);
-        pattern.push_back(head[i]);
-      }
-      break;
-    default:
-      if( head!=true_node ){
-        guards.push_back(head);
-        pattern.push_back( head );
-      }
-      break;
-    }
-    break;
-  default: Unreachable() << "RewriteRules can be of only three kinds"; break;
-  }
-  // Add the other guards
-  TNode g = r[1];
-  switch(g.getKind()){
-  case kind::AND:
-    for( unsigned i = 0; i<g.getNumChildren(); i++ ){
-      guards.push_back(g[i]);
-    }
-    break;
-  default:
-    if( g != true_node ){
-      guards.push_back( g );
-    }
-    break;
-  }
-  // Add the other triggers
-  if( r[2].getNumChildren() >= 3 ){
-    for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) {
-      pattern.push_back( r[2][2][0][i] );
-    }
-  }
-
-  Trace("rr-rewrite") << "Rule is " << r << std::endl;
-  Trace("rr-rewrite") << "Head is " << head << std::endl;
-  Trace("rr-rewrite") << "Patterns are ";
-  for( unsigned i=0; i<pattern.size(); i++ ){
-    Trace("rr-rewrite") << pattern[i] << " ";
-  }
-  Trace("rr-rewrite") << std::endl;
-
-  NodeBuilder<> forallB(kind::FORALL);
-  forallB << r[0];
-  Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) );
-  gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body );
-  gg = Rewriter::rewrite( gg );
-  forallB << gg;
-  NodeBuilder<> patternB(kind::INST_PATTERN);
-  patternB.append(pattern);
-  NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
-  //the entire rewrite rule is the first pattern
-  if( options::quantRewriteRules() ){
-    patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r );
-  }
-  patternListB << static_cast<Node>(patternB);
-  forallB << static_cast<Node>(patternListB);
-  Node rn = (Node) forallB;
-
-  return rn;
-}
-
 bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
   if( n.getKind()==FORALL ){
     return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
@@ -2272,17 +2174,14 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
 
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   Node prev = n;
-  if( n.getKind() == kind::REWRITE_RULE ){
-    n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n );
-  }else{
-    if( options::preSkolemQuant() ){
-      if( !isInst || !options::preSkolemQuantNested() ){
-        Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
-        //apply pre-skolemization to existential quantifiers
-        std::vector< TypeNode > fvTypes;
-        std::vector< TNode > fvs;
-        n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
-      }
+
+  if( options::preSkolemQuant() ){
+    if( !isInst || !options::preSkolemQuantNested() ){
+      Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      //apply pre-skolemization to existential quantifiers
+      std::vector< TypeNode > fvTypes;
+      std::vector< TNode > fvs;
+      n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
     }
   }
   //pull all quantifiers globally
@@ -2291,7 +2190,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   {
     Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
     std::map< unsigned, std::map< Node, Node > > visited;
-    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited );
+    n = computePrenexAgg( n, true, visited );
     n = Rewriter::rewrite( n );
     Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
     //Assert( isPrenexNormalForm( n ) );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index e8f069882..69e057c76 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -204,7 +204,6 @@ private:
 private:
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
-  static Node rewriteRewriteRule( Node r );
   static bool isPrenexNormalForm( Node n );
   /** preprocess
    *
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
deleted file mode 100644
index 9903456c9..000000000
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ /dev/null
@@ -1,309 +0,0 @@
-/*********************                                                        */
-/*! \file rewrite_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Rewrite engine module
- **
- ** This class manages rewrite rules for quantifiers
- **/
-
-#include "theory/quantifiers/rewrite_engine.h"
-
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers_engine.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-struct PrioritySort {
-  std::vector< double > d_priority;
-  bool operator() (int i,int j) {
-    return d_priority[i] < d_priority[j];
-  }
-};
-
-RewriteEngine::RewriteEngine(context::Context* c,
-                             QuantifiersEngine* qe,
-                             QuantConflictFind* qcf)
-    : QuantifiersModule(qe), d_qcf(qcf)
-{
-  d_needsSort = false;
-}
-
-double RewriteEngine::getPriority( Node f ) {
-  Node rr = QuantAttributes::getRewriteRule( f );
-  Node rrr = rr[2];
-  Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
-  bool deterministic = rrr[1].getKind()!=OR;
-
-  if( rrr.getKind()==RR_REWRITE ){
-    return deterministic ? 0.0 : 3.0;
-  }else if( rrr.getKind()==RR_DEDUCTION ){
-    return deterministic ? 1.0 : 4.0;
-  }else if( rrr.getKind()==RR_REDUCTION ){
-    return deterministic ? 2.0 : 5.0;
-  }else{
-    return 6.0;
-  }
-
-  //return deterministic ? 0.0 : 1.0;
-}
-
-bool RewriteEngine::needsCheck( Theory::Effort e ){
-  return e==Theory::EFFORT_FULL;
-  //return e>=Theory::EFFORT_LAST_CALL;
-}
-
-void RewriteEngine::check(Theory::Effort e, QEffort quant_e)
-{
-  if (quant_e == QEFFORT_STANDARD)
-  {
-    Assert(!d_quantEngine->inConflict());
-    Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
-    //if( e==Theory::EFFORT_LAST_CALL ){
-    //  if( !d_quantEngine->getModel()->isModelSet() ){
-    //    d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
-    //  }
-    //}
-    if( d_needsSort ){
-      d_priority_order.clear();
-      PrioritySort ps;
-      std::vector< int > indicies;
-      for( int i=0; i<(int)d_rr_quant.size(); i++ ){
-        ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
-        indicies.push_back( i );
-      }
-      std::sort( indicies.begin(), indicies.end(), ps );
-      for( unsigned i=0; i<indicies.size(); i++ ){
-        d_priority_order.push_back( d_rr_quant[indicies[i]] );
-      }
-      d_needsSort = false;
-    }
-
-    //apply rewrite rules
-    int addedLemmas = 0;
-    //per priority level
-    int index = 0;
-    bool success = true;
-    while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) {
-      addedLemmas += checkRewriteRule( d_priority_order[index], e );
-      index++;
-      if( index<(int)d_priority_order.size() ){
-        success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] );
-      }
-    }
-
-    Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
-  }
-}
-
-int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
-  Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl;
-
-  // get the proper quantifiers info
-  std::map<Node, QuantInfo>::iterator it = d_qinfo.find(f);
-  if (it == d_qinfo.end())
-  {
-    Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
-    return 0;
-  }
-  // reset QCF module
-  QuantInfo* qi = &it->second;
-  if (!qi->matchGeneratorIsValid())
-  {
-    Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl;
-    return 0;
-  }
-  d_qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT);
-  Node rr = QuantAttributes::getRewriteRule(f);
-  Trace("rewrite-engine-inst-debug") << "   Reset round..." << std::endl;
-  qi->reset_round(d_qcf);
-  Trace("rewrite-engine-inst-debug") << "   Get matches..." << std::endl;
-  int addedLemmas = 0;
-  while (!d_quantEngine->inConflict() && qi->getNextMatch(d_qcf)
-         && (addedLemmas == 0 || !options::rrOneInstPerRound()))
-  {
-    Trace("rewrite-engine-inst-debug")
-        << "   Got match to complete..." << std::endl;
-    qi->debugPrintMatch("rewrite-engine-inst-debug");
-    std::vector<int> assigned;
-    if (!qi->isMatchSpurious(d_qcf))
-    {
-      bool doContinue = false;
-      bool success = true;
-      int tempAddedLemmas = 0;
-      while (!d_quantEngine->inConflict() && tempAddedLemmas == 0 && success
-             && (addedLemmas == 0 || !options::rrOneInstPerRound()))
-      {
-        success = qi->completeMatch(d_qcf, assigned, doContinue);
-        doContinue = true;
-        if (success)
-        {
-          Trace("rewrite-engine-inst-debug")
-              << "   Construct match..." << std::endl;
-          std::vector<Node> inst;
-          qi->getMatch(inst);
-          if (Trace.isOn("rewrite-engine-inst-debug"))
-          {
-            Trace("rewrite-engine-inst-debug")
-                << "   Add instantiation..." << std::endl;
-            for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild;
-                 i++)
-            {
-              Trace("rewrite-engine-inst-debug") << "  " << f[0][i] << " -> ";
-              if (i < inst.size())
-              {
-                Trace("rewrite-engine-inst-debug") << inst[i] << std::endl;
-              }
-              else
-              {
-                Trace("rewrite-engine-inst-debug")
-                    << "OUT_OF_RANGE" << std::endl;
-                Assert(false);
-              }
-            }
-          }
-          // resize to remove auxiliary variables
-          if (inst.size() > f[0].getNumChildren())
-          {
-            inst.resize(f[0].getNumChildren());
-          }
-          if (d_quantEngine->getInstantiate()->addInstantiation(f, inst))
-          {
-            addedLemmas++;
-            tempAddedLemmas++;
-          }
-          else
-          {
-            Trace("rewrite-engine-inst-debug") << "   - failed." << std::endl;
-          }
-          Trace("rewrite-engine-inst-debug")
-              << "   Get next completion..." << std::endl;
-        }
-      }
-      Trace("rewrite-engine-inst-debug")
-          << "   - failed to complete." << std::endl;
-    }
-    else
-    {
-      Trace("rewrite-engine-inst-debug")
-          << "   - match is spurious." << std::endl;
-    }
-    Trace("rewrite-engine-inst-debug") << "   Get next match..." << std::endl;
-  }
-  d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas;
-  Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
-  return addedLemmas;
-}
-
-void RewriteEngine::registerQuantifier( Node f ) {
-  Node rr = QuantAttributes::getRewriteRule( f );
-  if (rr.isNull())
-  {
-    return;
-  }
-  Trace("rr-register") << "Register quantifier " << f << std::endl;
-  Trace("rr-register") << "  rewrite rule is : " << rr << std::endl;
-  d_rr_quant.push_back(f);
-  d_rr[f] = rr;
-  d_needsSort = true;
-  Trace("rr-register") << "  guard is : " << d_rr[f][1] << std::endl;
-
-  std::vector<Node> qcfn_c;
-
-  std::vector<Node> bvl;
-  bvl.insert(bvl.end(), f[0].begin(), f[0].end());
-
-  NodeManager* nm = NodeManager::currentNM();
-  std::vector<Node> cc;
-  // add patterns
-  for (unsigned i = 1, nchild = f[2].getNumChildren(); i < nchild; i++)
-  {
-    std::vector<Node> nc;
-    for (const Node& pat : f[2][i])
-    {
-      Node nn;
-      Node nbv = nm->mkBoundVar(pat.getType());
-      if (pat.getType().isBoolean() && pat.getKind() != APPLY_UF)
-      {
-        nn = pat.negate();
-      }
-      else
-      {
-        nn = pat.eqNode(nbv).negate();
-        bvl.push_back(nbv);
-      }
-      nc.push_back(nn);
-    }
-    if (!nc.empty())
-    {
-      Node n = nc.size() == 1 ? nc[0] : nm->mkNode(AND, nc);
-      Trace("rr-register-debug") << "  pattern is " << n << std::endl;
-      if (std::find(cc.begin(), cc.end(), n) == cc.end())
-      {
-        cc.push_back(n);
-      }
-    }
-  }
-  qcfn_c.push_back(nm->mkNode(BOUND_VAR_LIST, bvl));
-
-  std::vector<Node> body_c;
-  // add the guards
-  if (d_rr[f][1].getKind() == AND)
-  {
-    for (const Node& g : d_rr[f][1])
-    {
-      if (MatchGen::isHandled(g))
-      {
-        body_c.push_back(g.negate());
-      }
-    }
-  }
-  else if (d_rr[f][1] != d_quantEngine->getTermUtil()->d_true)
-  {
-    if (MatchGen::isHandled(d_rr[f][1]))
-    {
-      body_c.push_back(d_rr[f][1].negate());
-    }
-  }
-  // add the patterns to the body
-  body_c.push_back(cc.size() == 1 ? cc[0] : nm->mkNode(AND, cc));
-  // make the body
-  qcfn_c.push_back(body_c.size() == 1 ? body_c[0] : nm->mkNode(OR, body_c));
-  // make the quantified formula
-  d_qinfo_n[f] = nm->mkNode(FORALL, qcfn_c);
-  Trace("rr-register") << "  qcf formula is : " << d_qinfo_n[f] << std::endl;
-  d_qinfo[f].initialize(d_qcf, d_qinfo_n[f], d_qinfo_n[f][1]);
-}
-
-void RewriteEngine::assertNode( Node n ) {
-
-}
-
-bool RewriteEngine::checkCompleteFor( Node q ) { 
-  // by semantics of rewrite rules, saturation -> SAT 
-  return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
-}
-
-Node RewriteEngine::getInstConstNode( Node n, Node q ) {
-  std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
-  if( it==d_inst_const_node[q].end() ){
-    Node nn =
-        d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
-            n, q);
-    d_inst_const_node[q][n] = nn;
-    return nn;
-  }else{
-    return it->second;
-  }
-}
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
deleted file mode 100644
index 29aba0f1a..000000000
--- a/src/theory/quantifiers/rewrite_engine.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \file rewrite_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
-**/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__REWRITE_ENGINE_H
-#define CVC4__REWRITE_ENGINE_H
-
-#include <map>
-#include <vector>
-
-#include "expr/attribute.h"
-#include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/quant_conflict_find.h"
-#include "theory/quantifiers/quant_util.h"
-
-namespace CVC4 {
-namespace theory {
-
-/**
- * An attribute for marking a priority value for rewrite rules.
- */
-struct RrPriorityAttributeId
-{
-};
-typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
-
-namespace quantifiers {
-
-class RewriteEngine : public QuantifiersModule
-{
-  std::vector< Node > d_rr_quant;
-  std::vector< Node > d_priority_order;
-  std::map< Node, Node > d_rr;
-  /** explicitly provided patterns */
-  std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
-  /** get the quantifer info object */
-  std::map< Node, Node > d_qinfo_n;
-  std::map< Node, QuantInfo > d_qinfo;
-  double getPriority( Node f );
-  bool d_needsSort;
-  std::map< Node, std::map< Node, Node > > d_inst_const_node;
-  Node getInstConstNode( Node n, Node q );
-
- private:
-  int checkRewriteRule( Node f, Theory::Effort e );
-
- public:
-  RewriteEngine(context::Context* c,
-                QuantifiersEngine* qe,
-                QuantConflictFind* qcf);
-
-  bool needsCheck(Theory::Effort e) override;
-  void check(Theory::Effort e, QEffort quant_e) override;
-  void registerQuantifier(Node f) override;
-  void assertNode(Node n) override;
-  bool checkCompleteFor(Node q) override;
-  /** Identify this module */
-  std::string identify() const override { return "RewriteEngine"; }
-
- private:
-  /**
-   * A pointer to the quantifiers conflict find module of the quantifiers
-   * engine. This is the module that computes instantiations for rewrite rule
-   * quantifiers.
-   */
-  QuantConflictFind* d_qcf;
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index a83dbf541..e2c9043a1 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -141,91 +141,6 @@ struct QuantifierInstClosureTypeRule {
   }
 };/* struct QuantifierInstClosureTypeRule */
 
-
-class RewriteRuleTypeRule {
-public:
-
-  /**
-   * Compute the type for (and optionally typecheck) a term belonging
-   * to the theory of rewriterules.
-   *
-   * @param nodeManager the NodeManager in use
-   * @param n the node to compute the type of
-   * @param check if true, the node's type should be checked as well
-   * as computed.
-   */
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check)
-  {
-    Debug("typecheck-r") << "type check for rr " << n << std::endl;
-    Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren() == 3);
-    if( check ){
-      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
-        throw TypeCheckingExceptionPrivate(n[0],
-                     "first argument of rewrite rule is not bound var list");
-      }
-      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n[1],
-                     "guard of rewrite rule is not an actual guard");
-      }
-      if( n[2].getType(check) !=
-          TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){
-        throw TypeCheckingExceptionPrivate(n[2],
-                     "not a correct rewrite rule");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class RewriteRuleTypeRule */
-
-class RRRewriteTypeRule {
-public:
-
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::RR_REWRITE);
-    if( check ){
-      if( n[0].getType(check)!=n[1].getType(check) ){
-        throw TypeCheckingExceptionPrivate(n,
-                     "terms of rewrite rule are not equal");
-      }
-      if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
-        throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
-      }
-      if( n[0].getKind()!=kind::APPLY_UF ){
-        throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation");
-      }
-    }
-    return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
-  }
-};/* struct QuantifierReductionRuleRule */
-
-class RRRedDedTypeRule {
-public:
-
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::RR_REDUCTION
-           || n.getKind() == kind::RR_DEDUCTION);
-    if( check ){
-      if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean");
-      }
-      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean");
-      }
-      if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
-        throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
-      }
-      if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){
-        throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least");
-      }
-    }
-    return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
-  }
-};/* struct QuantifierReductionRuleRule */
-
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c7eafc3b8..80a493496 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -30,7 +30,6 @@
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/sep/theory_sep.h"
 #include "theory/theory_engine.h"
@@ -53,7 +52,6 @@ class QuantifiersEnginePrivate
         d_model_engine(nullptr),
         d_bint(nullptr),
         d_qcf(nullptr),
-        d_rr_engine(nullptr),
         d_sg_gen(nullptr),
         d_synth_e(nullptr),
         d_lte_part_inst(nullptr),
@@ -81,8 +79,6 @@ class QuantifiersEnginePrivate
   std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
   /** Conflict find mechanism for quantifiers */
   std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
-  /** rewrite rules utility */
-  std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
   /** subgoal generator */
   std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
   /** ceg instantiation */
@@ -111,7 +107,7 @@ class QuantifiersEnginePrivate
                   bool& needsBuilder)
   {
     // add quantifiers modules
-    if (options::quantConflictFind() || options::quantRewriteRules())
+    if (options::quantConflictFind())
     {
       d_qcf.reset(new quantifiers::QuantConflictFind(qe, c));
       modules.push_back(d_qcf.get());
@@ -150,11 +146,6 @@ class QuantifiersEnginePrivate
       // finite model finder has special ways of building the model
       needsBuilder = true;
     }
-    if (options::quantRewriteRules())
-    {
-      d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get()));
-      modules.push_back(d_rr_engine.get());
-    }
     if (options::ltePartialInst())
     {
       d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c));
@@ -397,16 +388,6 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority )
 
 void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
 {
-  if (!qa.d_rr.isNull())
-  {
-    if (d_private->d_rr_engine.get() == nullptr)
-    {
-      Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : "
-                          << q << std::endl;
-    }
-    // set rewrite engine as owner
-    setOwner(q, d_private->d_rr_engine.get(), 2);
-  }
   if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
   {
     if (d_private->d_synth_e.get() == nullptr)
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 3b11d8e54..6a404104f 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -35,7 +35,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
-  if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE
+  if ((parent.isClosure()
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
@@ -178,7 +178,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 
   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
-  if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE
+  if ((parent.isClosure()
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 150983187..ca50e2c83 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -797,11 +797,6 @@ set(regress_0_tests
   regress0/rels/relations-ops.smt2
   regress0/rels/rels-sharing-simp.cvc
   regress0/reset-assertions.smt2
-  regress0/rewriterules/datatypes.smt2
-  regress0/rewriterules/length_trick.smt2
-  regress0/rewriterules/native_arrays.smt2
-  regress0/rewriterules/relation.smt2
-  regress0/rewriterules/simulate_rewriting.smt2
   regress0/sep/dispose-1.smt2
   regress0/sep/dup-nemp.smt2
   regress0/sep/nemp.smt2
@@ -1344,7 +1339,6 @@ set(regress_1_tests
   regress1/push-pop/arith_lra_02.smt2
   regress1/push-pop/bug-fmf-fun-skolem.smt2
   regress1/push-pop/bug216.smt2
-  regress1/push-pop/bug326.smt2
   regress1/push-pop/fuzz_1.smt2
   regress1/push-pop/fuzz_10.smt2
   regress1/push-pop/fuzz_11.smt2
@@ -1542,15 +1536,6 @@ set(regress_1_tests
   regress1/rels/rel_tp_join_2_1.cvc
   regress1/rels/set-strat.cvc
   regress1/rels/strat.cvc
-  regress1/rewriterules/datatypes_sat.smt2
-  regress1/rewriterules/length_gen.smt2
-  regress1/rewriterules/length_gen_020.smt2
-  regress1/rewriterules/length_gen_020_sat.smt2
-  regress1/rewriterules/length_gen_040.smt2
-  regress1/rewriterules/length_gen_040_lemma.smt2
-  regress1/rewriterules/length_gen_040_lemma_trigger.smt2
-  regress1/rewriterules/reachability_back_to_the_future.smt2
-  regress1/rewriterules/read5.smt2
   regress1/rr-verify/bool-crci.sy
   regress1/rr-verify/bv-term-32.sy
   regress1/rr-verify/bv-term.sy
@@ -2179,12 +2164,6 @@ set(regression_disabled_tests
   regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
   regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
   regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
-  regress0/rewriterules/datatypes_clark.smt2
-  regress0/rewriterules/length.smt2
-  regress0/rewriterules/length_gen_n.smt2
-  regress0/rewriterules/length_gen_n_lemma.smt2
-  regress0/rewriterules/length_trick2.smt2
-  regress0/rewriterules/native_datatypes.smt2
   regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
   regress0/sets/setel-eq.smt2
   regress0/sets/sets-new.smt2
@@ -2322,20 +2301,6 @@ set(regression_disabled_tests
   # doing a coverage build with LFSC.
   regress1/quantifiers/set3.smt2
   regress1/rels/garbage_collect.cvc
-  regress1/rewriterules/datatypes2.smt2
-  regress1/rewriterules/datatypes3.smt2
-  regress1/rewriterules/datatypes_clark_quantification.smt2
-  regress1/rewriterules/length_gen_010.smt2
-  regress1/rewriterules/length_gen_010_lemma.smt2
-  regress1/rewriterules/length_gen_080.smt2
-  regress1/rewriterules/length_gen_160_lemma.smt2
-  regress1/rewriterules/length_gen_inv_160.smt2
-  regress1/rewriterules/length_trick3.smt2
-  regress1/rewriterules/length_trick3_int.smt2
-  regress1/rewriterules/set_A_new_fast_tableau-base.smt2
-  regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2
-  regress1/rewriterules/test_guards.smt2
-  regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2
   regress1/sets/setofsets-disequal.smt2
   regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
   regress1/simple-rdl-definefun.smt2
diff --git a/test/regress/regress0/rewriterules/datatypes.smt2 b/test/regress/regress0/rewriterules/datatypes.smt2
deleted file mode 100644
index 9a5f68100..000000000
--- a/test/regress/regress0/rewriterules/datatypes.smt2
+++ /dev/null
@@ -1,102 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; try to solve datatypes with rewriterules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; lists 2 nil
-(declare-sort elt 0) ;; we suppose that elt is infinite
-(declare-sort list 0)
-
-(declare-fun nil1 () list)
-(declare-fun nil2 () list)
-(declare-fun cons (elt list) list)
-
-;;;;;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj1 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj2 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun proj1 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj2 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun iscons (list) Bool)
-(assert (= (iscons nil1) false))
-(assert (= (iscons nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun isnil1 (list) Bool)
-(assert (= (isnil1 nil1) true))
-(assert (= (isnil1 nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) ))
-
-(declare-fun isnil2 (list) Bool)
-(assert (= (isnil2 nil1) false))
-(assert (= (isnil2 nil2) true))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) ))
-
-;; distinct
-(assert (forall ((?l list))
-                (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; finite case-split
-(assert (forall ((?l list))
-                 (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
-
-
-
-;;;;; goal
-
-(declare-fun e () elt)
-(declare-fun l1 () list)
-(declare-fun l2 () list)
-
-
-(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l1) (proj2 l2)))))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2
deleted file mode 100644
index cc217fc79..000000000
--- a/test/regress/regress0/rewriterules/datatypes_clark.smt2
+++ /dev/null
@@ -1,205 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIRA)
-
-;; DATATYPE
-;;   nat = succ(pred : nat) | zero,
-;;   list = cons(car : tree, cdr : list) | null,
-;;   tree = node(children : list) | leaf(data : nat)
-;; END;
-
-;;;;;;;;;;;
-;; nat   ;;
-;;;;;;;;;;;
-(declare-sort nat 0)
-(declare-fun zero () nat)
-(declare-fun succ (nat) nat)
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj1 (nat) nat)
-(assert-propagation((?x1 nat))
-                 (((succ ?x1))) () () (= (inj1 (succ ?x1)) ?x1) )
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun pred (nat) nat)
-(assert-rewrite ((?x1 nat)) () () (pred (succ ?x1)) ?x1 )
-
-(assert (= (pred zero) zero))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_succ (nat) Bool)
-(assert (= (is_succ zero) false))
-(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (= (is_succ (succ ?x1)) true) )
-
-(assert-propagation ((?x1 nat)) (((pred ?x1))) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1))))
-
-(declare-fun is_zero (nat) Bool)
-(assert (= (is_zero zero) true))
-(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (= ?x1 zero))
-
-;;; directrr
-(assert-rewrite ((?x1 nat)) () () (is_succ (succ ?x1)) true )
-(assert-rewrite ((?x1 nat)) () () (is_zero (succ ?x1)) false )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (not (is_succ ?x1)) )
-(assert-propagation ((?x1 nat)) () () ((is_succ ?x1)) (not (is_zero ?x1)) )
-(assert-propagation ((?x1 nat)) () () ((not (is_zero ?x1))) (is_succ ?x1) )
-(assert-propagation ((?x1 nat)) () () ((not (is_succ ?x1))) (is_zero ?x1) )
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert-propagation ((?x1 nat)) (((pred ?x1))) () () (or (is_zero ?x1) (is_succ ?x1)) )
-
-;;;;;;;;;;;;;;;;;;;
-;; non-cyclic
-(declare-fun size_nat (nat) Real)
-(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) )
-
-
-
-;;;;;;;;;;;;;;;;;;;;;
-;; list and tree
-
-(declare-sort list 0)
-(declare-sort tree 0)
-
-;;;;;;;;;;;
-;; list  ;;
-;;;;;;;;;;;
-
-(declare-fun null () list)
-(declare-fun cons (tree list) list)
-
-(declare-fun node (list) tree)
-(declare-fun leaf (nat) tree)
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj2 (list) tree)
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj2 (cons ?x1 ?x2)) ?x1) )
-
-(declare-fun inj3 (list) list)
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj3 (cons ?x1 ?x2)) ?x2) )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun car (list) tree)
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (car (cons ?x1 ?x2)) ?x1)
-
-(assert (= (car null) (node null)))
-
-(declare-fun cdr (list) list)
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (cdr (cons ?x1 ?x2)) ?x2)
-
-(assert (= (cdr null) null))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_cons (list) Bool)
-(assert (= (is_cons null) false))
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (is_cons (cons ?x1 ?x2)) true) )
-
-(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) )
-(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) )
-
-(declare-fun is_null (list) Bool)
-(assert (= (is_null null) true))
-
-(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_null ?x1)) (= (car ?x1) (node null)) )
-(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_null ?x1)) (= (cdr ?x1) null) )
-
-(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (= ?x1 null))
-
-;;; directrr
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_cons (cons ?x1 ?x2)) true)
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_null (cons ?x1 ?x2)) false)
-
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (not (is_cons ?x1)) )
-(assert-propagation ((?x1 list)) () () ((is_cons ?x1)) (not (is_null ?x1)) )
-(assert-propagation ((?x1 list)) () () ((not (is_null ?x1))) (is_cons ?x1) )
-(assert-propagation ((?x1 list)) () () ((not (is_cons ?x1))) (is_null ?x1) )
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert-propagation ((?x1 list)) (((car ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) )
-(assert-propagation ((?x1 list)) (((cdr ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) )
-
-;;;;;;;;;;;;;;;
-;; tree
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj4 (tree) list)
-(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (inj4 (node ?x1)) ?x1) )
-
-(declare-fun inj5 (tree) nat)
-(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (inj5 (leaf ?x1)) ?x1) )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun children (tree) list)
-(assert-rewrite ((?x1 list)) () () (children (node ?x1)) ?x1 )
-(assert-rewrite ((?x1 nat)) () () (children (leaf ?x1)) null )
-
-(declare-fun data (tree) nat)
-(assert-rewrite ((?x1 nat)) () () (data (leaf ?x1)) ?x1 )
-(assert-rewrite ((?x1 list)) () () (data (node ?x1)) zero )
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_node (tree) Bool)
-(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (is_node (node ?x1)) true) )
-
-(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) )
-(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_node ?x1)) (= (data ?x1) zero) )
-
-
-(declare-fun is_leaf (tree) Bool)
-(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (is_leaf (leaf ?x1)) true) )
-(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) )
-(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_leaf ?x1)) (= (children ?x1) null) )
-
-;;; directrr
-(assert-rewrite ((?x1 list)) () () (is_node (node ?x1)) true )
-(assert-rewrite ((?x1 list)) () () (is_leaf (node ?x1)) false )
-(assert-rewrite ((?x1 nat)) () () (is_leaf (leaf ?x1)) true )
-(assert-rewrite ((?x1 nat)) () () (is_node (leaf ?x1)) false )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert-propagation ((?x1 tree)) () () ((is_node ?x1)) (not (is_leaf ?x1)) )
-(assert-propagation ((?x1 tree)) () () ((is_leaf ?x1)) (not (is_node ?x1)) )
-(assert-propagation ((?x1 tree)) () () ((not (is_node ?x1))) (is_leaf ?x1) )
-(assert-propagation ((?x1 tree)) () () ((not (is_leaf ?x1))) (is_node ?x1) )
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert-propagation ((?x1 tree)) (((children ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) )
-(assert-propagation ((?x1 tree)) (((data ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) )
-
-
-;;;;;;;;;;;;;;;;;;
-;; non-cyclic
-(declare-fun size_list (list) Real)
-(declare-fun size_tree (tree) Real)
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) )
-(assert-propagation ((?x1 list)) (((node ?x1))) () () (> (size_tree (node ?x1)) (size_list ?x1)) )
-(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) )
diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2
deleted file mode 100644
index b144d7745..000000000
--- a/test/regress/regress0/rewriterules/length.smt2
+++ /dev/null
@@ -1,27 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (forall ((?l list)) (! (=> (= ?l nil) (= (length ?l) 0)) :rewrite-rule)))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule)))
-
-;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0))))
-
-;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1)))))
-
-
-(assert (not (= (length (cons 1 (cons  2 (cons 3 nil)))) 3)))
-
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_gen_n.smt2 b/test/regress/regress0/rewriterules/length_gen_n.smt2
deleted file mode 100644
index 7da2f6777..000000000
--- a/test/regress/regress0/rewriterules/length_gen_n.smt2
+++ /dev/null
@@ -1,46 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) ))))
-
-;; (assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (= (gen_cons (+ ?n 1) nil) (cons 1 (gen_cons ?n nil))) ))))
-
-(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=>
-        (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l))))
-        (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l))))
-     )))))
-
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2
deleted file mode 100644
index 7d65356ad..000000000
--- a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2
+++ /dev/null
@@ -1,44 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l)))))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l))))
-
-(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l))))))
-
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) ))))
-
-(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=>
-        (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l))))
-        (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l))))
-     )))))
-
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_trick.smt2 b/test/regress/regress0/rewriterules/length_trick.smt2
deleted file mode 100644
index e01e97b84..000000000
--- a/test/regress/regress0/rewriterules/length_trick.smt2
+++ /dev/null
@@ -1,33 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-
-
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule)))
-
-;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0))))
-
-;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1)))))
-
-
-(assert (not (= (length (cons 1 (cons  2 (cons 3 nil)))) 3)))
-
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_trick2.smt2 b/test/regress/regress0/rewriterules/length_trick2.smt2
deleted file mode 100644
index 8d47d9550..000000000
--- a/test/regress/regress0/rewriterules/length_trick2.smt2
+++ /dev/null
@@ -1,33 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-
-
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule)))
-
-;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0))))
-
-;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1)))))
-
-(assert (forall ((?a Int) (?b Int) (?l list))
-        (not (> (length (cons ?a (cons  ?b ?l))) (length ?l)))))
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2
deleted file mode 100644
index 83de7d8f4..000000000
--- a/test/regress/regress0/rewriterules/native_arrays.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; This example can't be done if we don't access the EqualityEngine of
-;; the theory of arrays
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-(declare-sort Index 0)
-(declare-sort Element 0)
-
-;;A dumb predicate for a simple example
-(declare-fun P (Element) Bool)
-
-(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () ()
-                (P (select (store ?a ?i1 ?e) ?i2)) true )
-
-(declare-fun a1 () (Array Index Element))
-(declare-fun a2 () (Array Index Element))
-(declare-fun a3 () (Array Index Element))
-(declare-fun i1 () Index)
-(declare-fun i2 () Index)
-(declare-fun e1 () Element)
-
-(assert (not (=>  (or (= a1 (store a2 i1 e1)) (= a1 (store a3 i1 e1))) (P (select a1 i2)) )))
-(check-sat)
-(exit)
-
-
-;; (declare-fun a1 () (Array Index Element))
-;; (declare-fun a2 () (Array Index Element))
-;; (declare-fun i1 () Index)
-;; (assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1))))
-;; (assert (not (= a1 a2)))
-;; (check-sat)
-;; (exit)
diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2
deleted file mode 100644
index 365ec0624..000000000
--- a/test/regress/regress0/rewriterules/native_datatypes.smt2
+++ /dev/null
@@ -1,34 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-info :status unsat)
-
-(declare-datatypes ((nat 0) (list 0)) (
-((succ (pred nat)) (zero ) )
-((cons (car nat)(cdr list)) (nil ) )
-
-))
-
-
-;;define length
-(declare-fun length (list) nat)
-
-(assert (= (length nil) zero))
-
-(assert (forall ((?e nat) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (nat list) list)
-
-(assert (forall ((?l list)) (! (= (gen_cons zero ?l) ?l) :rewrite-rule)))
-
-(assert (forall ((?n nat) (?l list)) (! (= (gen_cons (succ ?n) ?l)
-        (gen_cons ?n (cons zero ?l))) :rewrite-rule)))
-
-(declare-fun n () nat)
-
-(assert (not (= (length (gen_cons (succ (succ zero)) nil)) (succ (succ zero)))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2
deleted file mode 100644
index 6b55a9677..000000000
--- a/test/regress/regress0/rewriterules/relation.smt2
+++ /dev/null
@@ -1,28 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort elt 0)
-
-(declare-fun R (elt elt) Bool)
-
-;; reflexive
-(assert-rewrite ((x elt)) () () (R x x) true)
-
-;; transitive
-(assert-propagation ((x elt) (y elt) (z elt)) () () ((R x y) (R y z)) (R x z))
-
-;; anti-symmetric
-(assert-propagation ((x elt) (y elt)) () () ((R x y) (R y x)) (= x y))
-
-(declare-fun e1 () elt)
-(declare-fun e2 () elt)
-(declare-fun e3 () elt)
-(declare-fun e4 () elt)
-
-(assert (not (=> (and (R e1 e2) (R e2 e3) (R e3 e4) (R e4 e1)) (= e1 e4))))
-
-(check-sat)
-
-(exit)
\ No newline at end of file
diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2
deleted file mode 100644
index f67a0e6a2..000000000
--- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2
+++ /dev/null
@@ -1,25 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-(declare-sort elt1 0)
-(declare-sort elt2 0)
-
-(declare-fun g (elt2) Bool)
-
-(declare-fun p (elt1 elt1) Bool)
-(declare-fun f (elt2) elt1)
-(declare-fun c1 () elt1)
-(declare-fun c2 () elt1)
-
-(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c2)) :rewrite-rule)))
-(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c1)) :rewrite-rule)))
-
-(declare-fun e () elt2)
-
-(assert (not (=> (g e) (=> (p c1 c2) (p (f e) (f e)))) ))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/push-pop/bug326.smt2 b/test/regress/regress1/push-pop/bug326.smt2
deleted file mode 100644
index f1506b3e8..000000000
--- a/test/regress/regress1/push-pop/bug326.smt2
+++ /dev/null
@@ -1,41 +0,0 @@
-; COMMAND-LINE: --incremental --rewrite-rules
-
-(set-logic AUFLIA)
-
-(declare-fun R (Int Int) Bool)
-
-;; reflexive
-(assert-rewrite ((x Int)) () () (R x x) true)
-
-;; anti-symmetric
-(assert-reduction ((x Int) (y Int)) () () ((R x y) (R y x)) (= x y))
-
-;; transitive
-(assert-propagation ((x Int) (y Int) (z Int)) () () ((R x y) (R y z)) (R x z))
-
-
-(declare-fun e1 () Int)
-(declare-fun e2 () Int)
-(declare-fun e3 () Int)
-(declare-fun e4 () Int)
-
-; EXPECT: unsat
-(push);;unsat
-(assert (not (=> (and (R e1 e2) (R e2 e4) (R e1 e3) (R e3 e4) (= e1 e4)) (= e2 e3))))
-(check-sat)
-(pop)
-
-; EXPECT: unsat
-(push);;unsat
-(assert (not (=> (and (R e1 e2) (R e1 e3) (or (R e2 e4) (R e3 e4)) ) (R e1 e4))))
-(check-sat)
-(pop)
-
-; EXPECT: sat
-(push);;sat
-(assert (and (not (R e1 e3)) (R e4 e1)))
-(check-sat)
-(pop)
-
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/datatypes2.smt2 b/test/regress/regress1/rewriterules/datatypes2.smt2
deleted file mode 100644
index 4ef40597a..000000000
--- a/test/regress/regress1/rewriterules/datatypes2.smt2
+++ /dev/null
@@ -1,151 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; try to solve datatypes with rewriterules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; lists 2 nil
-(declare-sort elt 0) ;; we suppose that elt is infinite
-(declare-sort list 0)
-
-(declare-fun nil1 () list)
-(declare-fun nil2 () list)
-(declare-fun cons1 (elt list) list)
-(declare-fun cons2 (elt list) list)
-
-;;;;;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj11 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj12 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj21 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj22 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun proj11 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj12 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) ))
-
-
-(declare-fun proj21 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj22 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun iscons1 (list) Bool)
-(assert (= (iscons1 nil1) false))
-(assert (= (iscons1 nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons1 (cons2 ?e ?l)) false))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun iscons2 (list) Bool)
-(assert (= (iscons2 nil1) false))
-(assert (= (iscons2 nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons2 (cons1 ?e ?l)) false))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun isnil1 (list) Bool)
-(assert (= (isnil1 nil1) true))
-(assert (= (isnil1 nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil1 (cons1 ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil1 (cons2 ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) ))
-
-(declare-fun isnil2 (list) Bool)
-(assert (= (isnil2 nil1) false))
-(assert (= (isnil2 nil2) true))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil2 (cons1 ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil2 (cons2 ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) ))
-
-;; distinct
-(assert (forall ((?l list))
-                (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; finite case-split
-(assert (forall ((?l list))
-                 (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
-
-
-
-;;;;; goal
-
-(declare-fun e () elt)
-(declare-fun l1 () list)
-(declare-fun l2 () list)
-
-
- (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2)))))))
-
-;;(assert (= (cons1 l1 l2) (cons2 l1 l2)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/datatypes3.smt2 b/test/regress/regress1/rewriterules/datatypes3.smt2
deleted file mode 100644
index fb9d79121..000000000
--- a/test/regress/regress1/rewriterules/datatypes3.smt2
+++ /dev/null
@@ -1,138 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; try to solve datatypes with rewriterules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; lists 2 nil
-(declare-sort elt 0) ;; we suppose that elt is infinite
-(declare-sort list 0)
-
-(declare-fun nil1 () list)
-(declare-fun nil2 () list)
-(declare-fun cons1 (elt list) list)
-(declare-fun cons2 (elt list) list)
-
-;;;;;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj11 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj11 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj12 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj12 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj21 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj21 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj22 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj22 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun proj11 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj12 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) ))
-
-(assert (= (proj11 nil1) nil1))
-(assert (= (proj12 nil1) nil1))
-(assert (= (proj11 nil2) nil2))
-(assert (= (proj12 nil2) nil2))
-
-(declare-fun proj21 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj22 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) ))
-
-(assert (= (proj21 nil1) nil1))
-(assert (= (proj22 nil1) nil1))
-(assert (= (proj21 nil2) nil2))
-(assert (= (proj22 nil2) nil2))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun iscons1 (list) Bool)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun iscons2 (list) Bool)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun isnil1 (list) Bool)
-(assert (= (isnil1 nil1) true))
-
-(declare-fun isnil2 (list) Bool)
-(assert (= (isnil2 nil2) true))
-
-;; distinct
-(assert (forall ((?l list))
-                (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; finite case-split
-(assert (forall ((?l list))
-                 (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
-
-
-
-;;;;; goal
-
-(declare-fun e () elt)
-(declare-fun l1 () list)
-(declare-fun l2 () list)
-
-
-;; (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2)))))))
-
-(assert (= (cons1 l1 l2) (cons2 l1 l2)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 b/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2
deleted file mode 100644
index a8dc5227a..000000000
--- a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2
+++ /dev/null
@@ -1,265 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIRA)
-
-;; DATATYPE
-;;   nat = succ(pred : nat) | zero,
-;;   list = cons(car : tree, cdr : list) | null,
-;;   tree = node(children : list) | leaf(data : nat)
-;; END;
-
-;;;;;;;;;;;
-;; nat   ;;
-;;;;;;;;;;;
-(declare-sort nat 0)
-(declare-fun zero () nat)
-(declare-fun succ (nat) nat)
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj1 (nat) nat)
-(assert (forall ((?x1 nat))
-                (! (= (inj1 (succ ?x1)) ?x1) :pattern ((succ ?x1)) ) ))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun pred (nat) nat)
-(assert (forall ((?x1 nat))
-                (! (= (pred (succ ?x1)) ?x1) :pattern ((pred (succ ?x1))) ) ))
-
-(assert (= (pred zero) zero))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_succ (nat) Bool)
-(assert (= (is_succ zero) false))
-(assert (forall ((?x1 nat))
-                (! (= (is_succ (succ ?x1)) true) :pattern ((succ ?x1)) ) ))
-
-(assert (forall ((?x1 nat))
-                (! (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1)))) :pattern ((is_succ ?x1) (pred ?x1)) ) ))
-
-(declare-fun is_zero (nat) Bool)
-(assert (= (is_zero zero) true))
-(assert (forall ((?x1 nat))
-                (! (=> (is_zero ?x1) (= ?x1 zero)) :pattern ((is_zero ?x1)) ) ))
-
-;;; directrr
-(assert (forall ((?x1 nat))
-                (! (= (is_succ (succ ?x1)) true) :pattern ((is_succ (succ ?x1))) ) ))
-(assert (forall ((?x1 nat))
-                (! (= (is_zero (succ ?x1)) false) :pattern ((is_zero (succ ?x1))) )))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert (forall ((?x1 nat))
-                (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :pattern ((is_zero ?x1)) ) ))
-(assert (forall ((?x1 nat))
-                (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :pattern ((is_succ ?x1)) ) ))
-(assert (forall ((?x1 nat))
-                (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :pattern ((is_zero ?x1)) ) ))
-(assert (forall ((?x1 nat))
-                (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :pattern ((is_succ ?x1)) ) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?x1 nat))
-                (! (or (is_zero ?x1) (is_succ ?x1)) :pattern ((pred ?x1)) ) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; non-cyclic
-(declare-fun size_nat (nat) Real)
-(assert (forall ((?x1 nat))
-                (! (> (size_nat (succ ?x1)) (size_nat ?x1)) :pattern ((succ ?x1)) ) ))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;
-;; list and tree
-
-(declare-sort list 0)
-(declare-sort tree 0)
-
-;;;;;;;;;;;
-;; list  ;;
-;;;;;;;;;;;
-
-(declare-fun null () list)
-(declare-fun cons (tree list) list)
-
-(declare-fun node (list) tree)
-(declare-fun leaf (nat) tree)
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj2 (list) tree)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (inj2 (cons ?x1 ?x2)) ?x1) :pattern ((cons ?x1 ?x2)) ) ))
-
-(declare-fun inj3 (list) list)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (inj3 (cons ?x1 ?x2)) ?x2) :pattern ((cons ?x1 ?x2)) ) ))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun car (list) tree)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (car (cons ?x1 ?x2)) ?x1) :pattern ((car (cons ?x1 ?x2))) ) ))
-
-(assert (= (car null) (node null)))
-
-(declare-fun cdr (list) list)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (cdr (cons ?x1 ?x2)) ?x2) :pattern ((cdr (cons ?x1 ?x2))) ) ))
-
-(assert (= (cdr null) null))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_cons (list) Bool)
-(assert (= (is_cons null) false))
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((cons ?x1 ?x2)) ) ))
-
-(assert (forall ((?x1 list))
-                (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(car ?x1)) ) ))
-(assert (forall ((?x1 list))
-                (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(cdr ?x1)) ) ))
-
-(declare-fun is_null (list) Bool)
-(assert (= (is_null null) true))
-
-(assert (forall ((?x1 list))
-                (! (=> (is_null ?x1) (= (car ?x1) (node null))) :pattern ((is_null ?x1)(car ?x1)) )  ))
-(assert (forall ((?x1 list))
-                (! (=> (is_null ?x1) (= (cdr ?x1) null)) :pattern ((is_null ?x1)(cdr ?x1)) ) ))
-
-(assert (forall ((?x1 list))
-                (! (=> (is_null ?x1) (= ?x1 null)) :pattern ((is_null ?x1)) ) ))
-
-;;; directrr
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((is_cons (cons ?x1 ?x2))) ) ))
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (= (is_null (cons ?x1 ?x2)) false) :pattern ((is_null (cons ?x1 ?x2))) ) ))
-
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert (forall ((?x1 list))
-                (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :pattern ((is_null ?x1)) ) ))
-(assert (forall ((?x1 list))
-                (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :pattern ((is_cons ?x1)) ) ))
-(assert (forall ((?x1 list))
-                (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :pattern ((is_null ?x1)) ) ))
-(assert (forall ((?x1 list))
-                (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :pattern ((is_cons ?x1)) ) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?x1 list))
-            (!  (or (is_null ?x1) (is_cons ?x1)) :pattern ((car ?x1)) ) ))
-(assert (forall ((?x1 list))
-            (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((cdr ?x1)) ) ))
-
-;;;;;;;;;;;;;;;
-;; tree
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj4 (tree) list)
-(assert (forall ((?x1 list))
-                (! (= (inj4 (node ?x1)) ?x1) :pattern ((node ?x1)) ) ))
-
-(declare-fun inj5 (tree) nat)
-(assert (forall ((?x1 nat))
-                (!  (= (inj5 (leaf ?x1)) ?x1) :pattern ((leaf ?x1)) )  ))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun children (tree) list)
-(assert (forall ((?x1 list))
-                (! (= (children (node ?x1)) ?x1) :pattern ((children (node ?x1))) ) ))
-(assert (forall ((?x1 nat))
-                (! (= (children (leaf ?x1)) null) :pattern ((children (leaf ?x1))) ) ))
-
-
-(declare-fun data (tree) nat)
-(assert (forall ((?x1 nat))
-                (! (= (data (leaf ?x1)) ?x1) :pattern ((data (leaf ?x1))) ) ))
-(assert (forall ((?x1 list))
-                (! (= (data (node ?x1)) zero) :pattern ((data (node ?x1))) ) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_node (tree) Bool)
-(assert (forall ((?x1 list))
-                (! (= (is_node (node ?x1)) true) :pattern ((node ?x1)) )  ))
-
-(assert (forall ((?x1 tree))
-                (! (=> (is_node ?x1) (= ?x1 (node (children ?x1)))) :pattern ((is_node ?x1)(children ?x1)) ) ))
-
-(assert (forall ((?x1 tree))
-                (! (=> (is_node ?x1) (= (data ?x1) zero)) :pattern ((is_node ?x1)(data ?x1)) ) ))
-
-
-(declare-fun is_leaf (tree) Bool)
-(assert (forall ((?x1 nat))
-                (! (=> true (= (is_leaf (leaf ?x1)) true)) :pattern ((leaf ?x1)) ) ))
-
-(assert (forall ((?x1 tree))
-                (! (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1)))) :pattern ((is_leaf ?x1)(data ?x1)) ) ))
-(assert (forall ((?x1 tree))
-                (! (=> (is_leaf ?x1) (= (children ?x1) null)) :pattern ((is_leaf ?x1)(children ?x1)) ) ))
-
-;;; directrr
-(assert (forall ((?x1 list))
-                (! (= (is_node (node ?x1)) true) :pattern ((is_node (node ?x1))) ) ))
-(assert (forall ((?x1 list))
-                (! (= (is_leaf (node ?x1)) false) :pattern ((is_leaf (node ?x1))) ) ))
-(assert (forall ((?x1 nat))
-                (! (= (is_leaf (leaf ?x1)) true) :pattern (is_leaf (leaf ?x1)) ) ))
-(assert (forall ((?x1 nat))
-                (! (= (is_node (leaf ?x1)) false) :pattern ((is_node (leaf ?x1))) ) ))
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert (forall ((?x1 tree))
-                (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :pattern ((is_node ?x1)) ) ))
-(assert (forall ((?x1 tree))
-                (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :pattern ((is_leaf ?x1)) ) ))
-(assert (forall ((?x1 tree))
-                (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :pattern ((is_node ?x1)) ) ))
-(assert (forall ((?x1 tree))
-                (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :pattern ((is_leaf ?x1)) ) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?x1 tree))
-                (!  (or (is_node ?x1) (is_leaf ?x1)) :pattern ((children ?x1)) ) ))
-
-(assert (forall ((?x1 tree))
-                (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((data ?x1)) )  ))
-
-
-;;;;;;;;;;;;;;;;;;
-;; non-cyclic
-(declare-fun size_list (list) Real)
-(declare-fun size_tree (tree) Real)
-(assert (forall ((?x1 tree) (?x2 list))
-                (! (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) :pattern ((cons ?x1 ?x2)) ) ))
-(assert (forall ((?x1 list))
-                (! (> (size_tree (node ?x1)) (size_list ?x1)) :pattern ((node ?x1)) )  ))
-(assert (forall ((?x1 nat))
-                (! (> (size_tree (leaf ?x1)) (size_nat ?x1)) :pattern ((leaf ?x1)) ) ))
diff --git a/test/regress/regress1/rewriterules/datatypes_sat.smt2 b/test/regress/regress1/rewriterules/datatypes_sat.smt2
deleted file mode 100644
index 4b5b59435..000000000
--- a/test/regress/regress1/rewriterules/datatypes_sat.smt2
+++ /dev/null
@@ -1,102 +0,0 @@
-; COMMAND-LINE: --rewrite-rules --no-check-models
-;; try to solve datatypes with rewriterules
-(set-logic AUFLIA)
-(set-info :status sat)
-
-;; lists 2 nil
-(declare-sort elt 0) ;; we suppose that elt is infinite
-(declare-sort list 0)
-
-(declare-fun nil1 () list)
-(declare-fun nil2 () list)
-(declare-fun cons (elt list) list)
-
-;;;;;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj1 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj2 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun proj1 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj2 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun iscons (list) Bool)
-(assert (= (iscons nil1) false))
-(assert (= (iscons nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun isnil1 (list) Bool)
-(assert (= (isnil1 nil1) true))
-(assert (= (isnil1 nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) ))
-
-(declare-fun isnil2 (list) Bool)
-(assert (= (isnil2 nil1) false))
-(assert (= (isnil2 nil2) true))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) ))
-
-;; distinct
-(assert (forall ((?l list))
-                (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; finite case-split
-(assert (forall ((?l list))
-                 (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
-
-
-
-;;;;; goal
-
-(declare-fun e () elt)
-(declare-fun l1 () list)
-(declare-fun l2 () list)
-
-
-(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l2) (proj2 l2)))))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen.smt2 b/test/regress/regress1/rewriterules/length_gen.smt2
deleted file mode 100644
index df876ef08..000000000
--- a/test/regress/regress1/rewriterules/length_gen.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 42 nil)) 42)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_010.smt2 b/test/regress/regress1/rewriterules/length_gen_010.smt2
deleted file mode 100644
index aee09cc96..000000000
--- a/test/regress/regress1/rewriterules/length_gen_010.smt2
+++ /dev/null
@@ -1,37 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-;; (assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(assert-rewrite ((?e Int) (?l list)) () () (length (cons ?e ?l)) (+ 1 (length ?l)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert-rewrite ((?n Int) (?l list)) () (= ?n 0) (gen_cons ?n ?l) (?l))
-
-(assert-rewrite ((?n Int) (?l list)) () (> ?n 0) (gen_cons ?n ?l)
-              (gen_cons (- ?n 1) (cons 1 ?l)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 10 nil)) 10)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2
deleted file mode 100644
index 49e6f970d..000000000
--- a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l)))))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l))))
-
-(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l))))))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 10 nil)) 10)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_020.smt2 b/test/regress/regress1/rewriterules/length_gen_020.smt2
deleted file mode 100644
index b7c2e5fd2..000000000
--- a/test/regress/regress1/rewriterules/length_gen_020.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 20 nil)) 20)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2
deleted file mode 100644
index 72db8d18b..000000000
--- a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules --no-check-models
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status sat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 20 nil)) 200)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_040.smt2 b/test/regress/regress1/rewriterules/length_gen_040.smt2
deleted file mode 100644
index 93a04cb7c..000000000
--- a/test/regress/regress1/rewriterules/length_gen_040.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 40 nil)) 40)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2
deleted file mode 100644
index cabd84575..000000000
--- a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l)))))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l))))
-
-(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l))))))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 40 nil)) 40)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2
deleted file mode 100644
index 7530269e8..000000000
--- a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2
+++ /dev/null
@@ -1,36 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) )))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) )))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l))))
-         :pattern ((gen_cons ?n ?l)) )))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 40 nil)) 40)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_080.smt2 b/test/regress/regress1/rewriterules/length_gen_080.smt2
deleted file mode 100644
index 451ea091e..000000000
--- a/test/regress/regress1/rewriterules/length_gen_080.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 80 nil)) 80)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2
deleted file mode 100644
index 7a81652ea..000000000
--- a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l)))))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l))))
-
-(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l))))))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 160 nil)) 160)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 b/test/regress/regress1/rewriterules/length_gen_inv_160.smt2
deleted file mode 100644
index af134287d..000000000
--- a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (cons 1 (gen_cons (- ?n 1) ?l)))) :rewrite-rule)))
-
-(declare-fun n () Int)
-
-(assert (not (= (length (gen_cons 160 nil)) 160)))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_trick3.smt2 b/test/regress/regress1/rewriterules/length_trick3.smt2
deleted file mode 100644
index fce35d691..000000000
--- a/test/regress/regress1/rewriterules/length_trick3.smt2
+++ /dev/null
@@ -1,37 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-;; don't use arith
-(declare-sort mynat 0)
-(declare-fun zero () mynat)
-(declare-fun succ (mynat) mynat)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) mynat)
-
-(assert (= (length nil) zero))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule)))
-
-(declare-fun ten_one_cons (list) list)
-
-(assert (forall ((?l list)) (! (= (ten_one_cons ?l)
-        (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) )))))))))
-        ) :rewrite-rule)))
-
-(assert (not (= (length (ten_one_cons nil))
-        (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero)))))))))))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/length_trick3_int.smt2 b/test/regress/regress1/rewriterules/length_trick3_int.smt2
deleted file mode 100644
index ec10ed6d3..000000000
--- a/test/regress/regress1/rewriterules/length_trick3_int.smt2
+++ /dev/null
@@ -1,45 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun ten_one_cons (list) list)
-
-(assert (forall ((?l list)) (! (= (ten_one_cons ?l)
-        (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) )))))))))
-        ) :rewrite-rule)))
-
-(assert (not (= (length (ten_one_cons nil))
-        10)))
-
-(check-sat)
-
-(declare-fun ten_one_ten (list) list)
-
-(assert (forall ((?l list)) (! (= (ten_one_ten ?l)
-        (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons ?l) )))))))))
-        ) :rewrite-rule)))
-
-(declare-fun two_one_ten (list) list)
-
-(assert (forall ((?l list)) (! (= (two_one_ten ?l)
-        (ten_one_cons (ten_one_cons ?l))
-        ) :rewrite-rule)))
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2
deleted file mode 100644
index b73f1b2a4..000000000
--- a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2
+++ /dev/null
@@ -1,55 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-(declare-sort elt 0)
-
-(declare-fun f (elt) elt)
-(declare-fun Rf (elt elt elt) Bool)
-
-;;eq
-(assert-propagation ((?x elt)) ((?x)) () () (or (= ?x ?x) (not (= ?x ?x))) )
-;; reflexive
-(assert-propagation ((?x elt)) ((?x)) () () (Rf ?x ?x ?x) )
-;; step
-(assert-propagation ((?x elt)) (((f ?x))) () () (Rf ?x (f ?x) (f ?x)) )
-;; reach
-(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) )
-;; cycle
-(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) )
-;; sandwich
-(assert-propagation ((?x1 elt)(?x2 elt)) () () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) )
-;; order1
-(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3))
-                    (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) )
-;; order2
-(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x3))
-                    (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) )
-;; transitive1
-(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3))
-                    (Rf ?x1 ?x3 ?x3) )
-;; transitive2
-(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2))
-                    (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) )
-;;transitive3
-(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1))
-                    (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) )
-
-(declare-fun e1 () elt)
-(declare-fun e2 () elt)
-(declare-fun e3 () elt)
-(declare-fun e4 () elt)
-
-
-;; (assert (=> (Rf e1 e2 e3) (Rf e1 (f e1) (f e1)) ))
-
-;; (assert (=> (Rf e1 e2 e3) (Rf e1 e3 e3) ))
-
-;; (assert (=> (Rf e1 e2 e3) (or (= e1 e3) (Rf e1 (f e1) e3)) ))
-
-(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3) )))
-
-
-(check-sat)
-(exit)
\ No newline at end of file
diff --git a/test/regress/regress1/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2
deleted file mode 100644
index 0f92effcb..000000000
--- a/test/regress/regress1/rewriterules/read5.smt2
+++ /dev/null
@@ -1,36 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUF)
-(set-info :source |
-Translated from old SVC processor verification benchmarks.  Contact Clark
-Barrett at barrett@cs.stanford.edu for more information.
-
-This benchmark was automatically translated into SMT-LIB format from
-CVC format using CVC Lite
-|)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(set-info :status unsat)
-(declare-sort Index 0)
-(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index)
-(declare-fun a () Index)
-(declare-fun aaa () Index)
-(declare-fun aa () Index)
-(declare-fun S () Arr)
-(declare-fun vvv () Element)
-(declare-fun v () Element)
-(declare-fun vv () Element)
-(declare-fun bbb () Index)
-(declare-fun www () Element)
-(declare-fun bb () Index)
-(declare-fun ww () Element)
-(declare-fun b () Index)
-(declare-fun w () Element)
-(declare-fun SS () Arr)
-(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false))))
-; rewrite rule definition of arrays theory
-(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule)))
-(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule)))
-(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule)))
-(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule)))
-(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat)
-(exit)
diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2
deleted file mode 100644
index 7434f4257..000000000
--- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2
+++ /dev/null
@@ -1,127 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort elt 0)
-(declare-sort set 0)
-
-(declare-fun in (elt set) Bool)
-
-;;;;;;;;;;;;;;;;;;;;
-;; inter
-
-(declare-fun inter (set set)  set)
-(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
-
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
-
-;;;;;;;;;;;;;;;;;
-;; union
-
-(declare-fun union (set set)  set)
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
-
-;;;;;;;;;;;;;;;;;;;;
-;; diff
-
-(declare-fun diff (set set)  set)
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
-
-;;;;;;;;;;;;;;;;
-;;sing
-
-(declare-fun sing (elt)  set)
-(assert-propagation ((?s elt))
-                   (((sing ?s))) () () (in ?s (sing ?s)) )
-
-(assert-propagation ((?s elt) (?t1 elt))
-                   () () ((in ?s (sing ?t1))) (= ?s ?t1))
-
-(assert-propagation ((?s elt) (?t1 elt))
-                   () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
-
-;;;;;;;;;;;;;;;;;;;
-;; fullfiling runned at Full effort
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
-
-(assert-propagation ((?t1 set) (?t2 set))
-                   () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
-
-;;;;;;;;;;;;;;;;;;;
-;; shortcut
-(declare-fun subset (set set) Bool)
-(assert-reduction ((?t1 set) (?t2 set))
-                 () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
-
-(declare-fun e () elt)
-(declare-fun t1 () set)
-(declare-fun t2 () set)
-(declare-fun t3 () set)
-
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
-
-;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
-
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
-
-;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) )
-(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) )
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2
deleted file mode 100644
index 256c9bb11..000000000
--- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2
+++ /dev/null
@@ -1,128 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
-(set-logic AUFLIA)
-(set-info :status sat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort elt 0)
-(declare-sort set 0)
-
-(declare-fun in (elt set) Bool)
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; inter
-
-(declare-fun inter (set set)  set)
-(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
-
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
-
-;;;;;;;;;;;;;;;;;
-;; union
-
-(declare-fun union (set set)  set)
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
-
-;;;;;;;;;;;;;;;;;;;;
-;; diff
-
-(declare-fun diff (set set)  set)
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
-
-;;;;;;;;;;;;;;;;
-;;sing
-
-(declare-fun sing (elt)  set)
-(assert-propagation ((?s elt))
-                  (((sing ?s))) () () (in ?s (sing ?s)) )
-
-(assert-propagation ((?s elt) (?t1 elt))
-                  () () ((in ?s (sing ?t1))) (= ?s ?t1))
-
-(assert-propagation ((?s elt) (?t1 elt))
-                  () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
-
-;;;;;;;;;;;;;;;;;;;
-;; fullfiling runned at Full effort
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
-
-(assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
-
-(assert-propagation ((?t1 set) (?t2 set))
-                  () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
-
-;;;;;;;;;;;;;;;;;;;
-;; shortcut
-(declare-fun subset (set set) Bool)
-(assert-reduction ((?t1 set) (?t2 set))
-                () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
-
-(declare-fun e () elt)
-(declare-fun t1 () set)
-(declare-fun t2 () set)
-(declare-fun t3 () set)
-
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
-
-;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
-
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
-
-(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) )
-
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/test_guards.smt2 b/test/regress/regress1/rewriterules/test_guards.smt2
deleted file mode 100644
index 7344dfba5..000000000
--- a/test/regress/regress1/rewriterules/test_guards.smt2
+++ /dev/null
@@ -1,46 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-;; don't use arith
-(declare-sort mynat 0)
-(declare-fun zero () mynat)
-(declare-fun succ (mynat) mynat)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-(declare-fun p (list) Bool)
-
-
-;;define length
-(declare-fun length (list) mynat)
-
-(assert (= (length nil) zero))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule)))
-
-(declare-fun ten_one_cons (list) list)
-
-(assert (forall ((?l list)) (! (=> (p ?l) (= (ten_one_cons ?l)
-        (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) )))))))))
-        )) :rewrite-rule)))
-
-(declare-fun a  () Bool)
-(declare-fun b  () Bool)
-(declare-fun c  () Bool)
-
-(assert (=> a (p nil)) )
-(assert (=> b (p nil)) )
-(assert (or a b))
-
-(assert (not (= (length (ten_one_cons nil))
-        (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero)))))))))))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 b/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2
deleted file mode 100644
index 5646cd70b..000000000
--- a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2
+++ /dev/null
@@ -1,493 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;;; From a verification condition generated by why3. The original program
-;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html .
-;; The problem has been modified by doubling the size of the arrays
-;; (* **)
-;;    VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html **)
-;;    Problem 1: maximum /\ sum of an array **)
-
-;;    Author: Jean-Christophe Filliatre (CNRS) **)
-;;    Tool:   Why3 (see http://why3.lri.fr/) **)
-;; *\) **)
-
-;; Particularly the assertion in the test case that the sum s = 90
-
-;;; this is a prelude for CVC4
-(set-logic AUFNIRA)
-;;; this is a prelude for CVC4 integer arithmetic
-(declare-sort uni 0)
-
-(declare-sort deco 0)
-
-(declare-sort ty 0)
-
-(declare-fun sort (ty uni) deco)
-
-(declare-fun int () ty)
-
-(declare-fun real () ty)
-
-(declare-fun bool () ty)
-
-(declare-fun True () uni)
-
-(declare-fun False () uni)
-
-(declare-fun match_bool (deco deco deco) uni)
-
-;; match_bool_True
-  (assert
-  (forall ((a ty))
-  (forall ((z uni) (z1 uni))
-  (= (sort a (match_bool (sort bool True) (sort a z) (sort a z1))) (sort a z)))))
-
-;; match_bool_False
-  (assert
-  (forall ((a ty))
-  (forall ((z uni) (z1 uni))
-  (= (sort a (match_bool (sort bool False) (sort a z) (sort a z1))) (sort a
-                                                                    z1)))))
-
-(declare-fun index_bool (deco) Int)
-
-;; index_bool_True
-  (assert (= (index_bool (sort bool True)) 0))
-
-;; index_bool_False
-  (assert (= (index_bool (sort bool False)) 1))
-
-;; bool_inversion
-  (assert
-  (forall ((u uni))
-  (or (= (sort bool u) (sort bool True)) (= (sort bool u) (sort bool False)))))
-
-(declare-fun tuple0 () ty)
-
-(declare-fun Tuple0 () uni)
-
-;; tuple0_inversion
-  (assert (forall ((u uni)) (= (sort tuple0 u) (sort tuple0 Tuple0))))
-
-;; CompatOrderMult
-  (assert
-  (forall ((x Int) (y Int) (z Int))
-  (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z))))))
-
-(declare-fun ref (ty) ty)
-
-(declare-fun mk_ref (deco) uni)
-
-(declare-fun contents (deco) uni)
-
-;; contents_def
-  (assert
-  (forall ((a ty))
-  (forall ((u uni))
-  (= (sort a (contents (sort (ref a) (mk_ref (sort a u))))) (sort a u)))))
-
-;; ref_inversion
-  (assert
-  (forall ((a ty))
-  (forall ((u uni))
-  (= (sort (ref a) u) (sort (ref a)
-                      (mk_ref (sort a (contents (sort (ref a) u)))))))))
-
-(declare-fun map (ty ty) ty)
-
-(declare-fun get (deco deco) uni)
-
-(declare-fun set (deco deco deco) uni)
-
-;; Select_eq
-  (assert
-  (forall ((m (Array Int Int)))
-  (forall ((a1 Int) (a2 Int))
-  (forall ((b Int))
-  (! (=> (= a1 a2) (= (select (store m a1 b) a2) b)) :pattern ((select (store m a1 b) a2)) )))))
-
-;; Select_eq
-  (assert
-  (forall ((a ty) (b ty))
-  (forall ((m uni))
-  (forall ((a1 uni) (a2 uni))
-  (forall ((b1 uni))
-  (! (=> (= (sort a a1) (sort a a2))
-     (= (sort b
-        (get
-        (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1)))
-        (sort a a2))) (sort b b1))) :pattern ((sort b
-                                              (get
-                                              (sort (map a b)
-                                              (set (sort (map a b) m)
-                                              (sort a a1) (sort b b1)))
-                                              (sort a a2)))) ))))))
-
-;; Select_neq
-  (assert
-  (forall ((m (Array Int Int)))
-  (forall ((a1 Int) (a2 Int))
-  (forall ((b Int))
-  (! (=> (not (= a1 a2)) (= (select (store m a1 b) a2) (select m a2))) :pattern ((select (store m a1 b) a2)) )))))
-
-;; Select_neq
-  (assert
-  (forall ((a ty) (b ty))
-  (forall ((m uni))
-  (forall ((a1 uni) (a2 uni))
-  (forall ((b1 uni))
-  (! (=> (not (= (sort a a1) (sort a a2)))
-     (= (sort b
-        (get
-        (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1)))
-        (sort a a2))) (sort b (get (sort (map a b) m) (sort a a2))))) :pattern (
-  (sort b
-  (get (sort (map a b) (set (sort (map a b) m) (sort a a1) (sort b b1)))
-  (sort a a2)))) ))))))
-
-(declare-fun const1 (deco) uni)
-
-(declare-fun const2 (Int) (Array Int Int))
-
-;; Const
-  (assert (forall ((b Int) (a Int)) (= (select (const2 b) a) b)))
-
-;; Const
-  (assert
-  (forall ((a ty) (b ty))
-  (forall ((b1 uni) (a1 uni))
-  (= (sort b (get (sort (map a b) (const1 (sort b b1))) (sort a a1))) 
-  (sort b b1)))))
-
-(declare-sort array 1)
-
-(declare-fun array1 (ty) ty)
-
-(declare-fun mk_array (Int deco) uni)
-
-(declare-fun mk_array1 (Int (Array Int Int)) (array Int))
-
-(declare-fun length (deco) Int)
-
-(declare-fun t2tb ((array Int)) uni)
-
-(declare-fun tb2t (deco) (array Int))
-
-;; BridgeL
-  (assert
-  (forall ((i (array Int)))
-  (! (= (tb2t (sort (array1 int) (t2tb i))) i) :pattern ((sort (array1 int)
-                                                         (t2tb i))) )))
-
-;; BridgeR
-  (assert
-  (forall ((j uni))
-  (! (= (sort (array1 int) (t2tb (tb2t (sort (array1 int) j)))) (sort
-                                                                (array1 int)
-                                                                j)) :pattern (
-  (sort (array1 int) (t2tb (tb2t (sort (array1 int) j))))) )))
-
-;; length_def
-  (assert
-  (forall ((u Int) (u1 (Array Int Int)))
-  (= (length (sort (array1 int) (t2tb (mk_array1 u u1)))) u)))
-
-;; length_def
-  (assert
-  (forall ((a ty))
-  (forall ((u Int) (u1 uni))
-  (= (length (sort (array1 a) (mk_array u (sort (map int a) u1)))) u))))
-
-(declare-fun elts (deco) uni)
-
-(declare-fun t2tb1 ((Array Int Int)) uni)
-
-(declare-fun tb2t1 (deco) (Array Int Int))
-
-;; BridgeL
-  (assert
-  (forall ((i (Array Int Int)))
-  (! (= (tb2t1 (sort (map int int) (t2tb1 i))) i) :pattern ((sort
-                                                            (map int int)
-                                                            (t2tb1 i))) )))
-
-;; BridgeR
-  (assert
-  (forall ((j uni))
-  (! (= (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j)))) (sort
-                                                                    (map 
-                                                                    int 
-                                                                    int) j)) :pattern (
-  (sort (map int int) (t2tb1 (tb2t1 (sort (map int int) j))))) )))
-
-;; elts_def
-  (assert
-  (forall ((u Int) (u1 (Array Int Int)))
-  (= (tb2t1
-     (sort (map int int) (elts (sort (array1 int) (t2tb (mk_array1 u u1)))))) u1)))
-
-;; elts_def
-  (assert
-  (forall ((a ty))
-  (forall ((u Int) (u1 uni))
-  (= (sort (map int a)
-     (elts (sort (array1 a) (mk_array u (sort (map int a) u1))))) (sort
-                                                                  (map int a)
-                                                                  u1)))))
-
-;; array_inversion
-  (assert
-  (forall ((u (array Int)))
-  (= u (mk_array1 (length (sort (array1 int) (t2tb u)))
-       (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb u)))))))))
-
-;; array_inversion
-  (assert
-  (forall ((a ty))
-  (forall ((u uni))
-  (= (sort (array1 a) u) (sort (array1 a)
-                         (mk_array (length (sort (array1 a) u))
-                         (sort (map int a) (elts (sort (array1 a) u)))))))))
-
-(declare-fun get1 (deco Int) uni)
-
-(declare-fun t2tb2 (Int) uni)
-
-(declare-fun tb2t2 (deco) Int)
-
-;; BridgeL
-  (assert
-  (forall ((i Int))
-  (! (= (tb2t2 (sort int (t2tb2 i))) i) :pattern ((sort int (t2tb2 i))) )))
-
-;; BridgeR
-  (assert
-  (forall ((j uni))
-  (! (= (sort int (t2tb2 (tb2t2 (sort int j)))) (sort int j)) :pattern (
-  (sort int (t2tb2 (tb2t2 (sort int j))))) )))
-
-;; get_def
-  (assert
-  (forall ((a (array Int)) (i Int))
-  (= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) i))) (select 
-  (tb2t1 (sort (map int int) (elts (sort (array1 int) (t2tb a))))) i))))
-
-;; get_def
-  (assert
-  (forall ((a ty))
-  (forall ((a1 uni) (i Int))
-  (= (sort a (get1 (sort (array1 a) a1) i)) (sort a
-                                            (get
-                                            (sort (map int a)
-                                            (elts (sort (array1 a) a1)))
-                                            (sort int (t2tb2 i))))))))
-
-(declare-fun set1 (deco Int deco) uni)
-
-;; set_def
-  (assert
-  (forall ((a (array Int)) (i Int) (v Int))
-  (= (tb2t
-     (sort (array1 int)
-     (set1 (sort (array1 int) (t2tb a)) i (sort int (t2tb2 v))))) (mk_array1
-                                                                  (length
-                                                                  (sort
-                                                                  (array1
-                                                                  int)
-                                                                  (t2tb a)))
-                                                                  (store 
-                                                                  (tb2t1
-                                                                  (sort
-                                                                  (map 
-                                                                  int 
-                                                                  int)
-                                                                  (elts
-                                                                  (sort
-                                                                  (array1
-                                                                  int)
-                                                                  (t2tb a))))) i v)))))
-
-;; set_def
-  (assert
-  (forall ((a ty))
-  (forall ((a1 uni) (i Int) (v uni))
-  (= (sort (array1 a) (set1 (sort (array1 a) a1) i (sort a v))) (sort
-                                                                (array1 a)
-                                                                (mk_array
-                                                                (length
-                                                                (sort
-                                                                (array1 a)
-                                                                a1))
-                                                                (sort
-                                                                (map int a)
-                                                                (set
-                                                                (sort
-                                                                (map int a)
-                                                                (elts
-                                                                (sort
-                                                                (array1 a)
-                                                                a1)))
-                                                                (sort 
-                                                                int
-                                                                (t2tb2 i))
-                                                                (sort a v)))))))))
-
-(declare-fun make (Int deco) uni)
-
-;; make_def
-  (assert
-  (forall ((n Int) (v Int))
-  (= (tb2t (sort (array1 int) (make n (sort int (t2tb2 v))))) (mk_array1 n
-                                                              (const2 v)))))
-
-;; make_def
-  (assert
-  (forall ((a ty))
-  (forall ((n Int) (v uni))
-  (= (sort (array1 a) (make n (sort a v))) (sort (array1 a)
-                                           (mk_array n
-                                           (sort (map int a)
-                                           (const1 (sort a v)))))))))
-
-(declare-fun sum ((Array Int Int) Int Int) Int)
-
-;; Sum_def_empty
-  (assert
-  (forall ((c (Array Int Int)) (i Int) (j Int))
-  (=> (<= j i) (= (sum c i j) 0))))
-
-;; Sum_def_non_empty
-  (assert
-  (forall ((c (Array Int Int)) (i Int) (j Int))
-  (=> (< i j) (= (sum c i j) (+ (select c i) (sum c (+ i 1) j))))))
-
-;; Sum_right_extension
-  (assert
-  (forall ((c (Array Int Int)) (i Int) (j Int))
-  (=> (< i j) (= (sum c i j) (+ (sum c i (- j 1)) (select c (- j 1)))))))
-
-;; Sum_transitivity
-  (assert
-  (forall ((c (Array Int Int)) (i Int) (k Int) (j Int))
-  (=> (and (<= i k) (<= k j)) (= (sum c i j) (+ (sum c i k) (sum c k j))))))
-
-;; Sum_eq
-  (assert
-  (forall ((c1 (Array Int Int)) (c2 (Array Int Int)) (i Int) (j Int))
-  (=>
-  (forall ((k Int))
-  (=> (and (<= i k) (< k j)) (= (select c1 k) (select c2 k))))
-  (= (sum c1 i j) (sum c2 i j)))))
-
-(declare-fun sum1 ((array Int) Int Int) Int)
-
-;; sum_def
-  (assert
-  (forall ((a (array Int)) (l Int) (h Int))
-  (= (sum1 a l h) (sum
-                  (tb2t1
-                  (sort (map int int) (elts (sort (array1 int) (t2tb a))))) l
-                  h))))
-
-(declare-fun is_max ((array Int) Int Int Int) Bool)
-
-;; is_max_def
-  (assert
-  (forall ((a (array Int)) (l Int) (h Int) (m Int))
-  (and
-  (=> (is_max a l h m)
-  (and
-  (forall ((k Int))
-  (=> (and (<= l k) (< k h))
-  (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m)))
-  (or (and (<= h l) (= m 0))
-  (and (< l h)
-  (exists ((k Int))
-  (and (and (<= l k) (< k h))
-  (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))))
-  (=>
-  (and
-  (forall ((k Int))
-  (=> (and (<= l k) (< k h))
-  (<= (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))) m)))
-  (or (and (<= h l) (= m 0))
-  (and (< l h)
-  (exists ((k Int))
-  (and (and (<= l k) (< k h))
-  (= m (tb2t2 (sort int (get1 (sort (array1 int) (t2tb a)) k))))))))) (is_max
-  a l h m)))))
-
-(assert
-;; WP_parameter_test_case
- ;; File "vstte10_max_sum/../vstte10_max_sum.mlw", line 63, characters 6-15
-  (not
-  (=> (<= 0 20)
-  (=> (and (<= 0 0) (< 0 20))
-  (forall ((a (Array Int Int)))
-  (=> (= a (store (const2 0) 0 9))
-  (=> (and (<= 0 1) (< 1 20))
-  (forall ((a1 (Array Int Int)))
-  (=> (= a1 (store a 1 5))
-  (=> (and (<= 0 2) (< 2 20))
-  (forall ((a2 (Array Int Int)))
-  (=> (= a2 (store a1 2 0))
-  (=> (and (<= 0 3) (< 3 20))
-  (forall ((a3 (Array Int Int)))
-  (=> (= a3 (store a2 3 2))
-  (=> (and (<= 0 4) (< 4 20))
-  (forall ((a4 (Array Int Int)))
-  (=> (= a4 (store a3 4 7))
-  (=> (and (<= 0 5) (< 5 20))
-  (forall ((a5 (Array Int Int)))
-  (=> (= a5 (store a4 5 3))
-  (=> (and (<= 0 6) (< 6 20))
-  (forall ((a6 (Array Int Int)))
-  (=> (= a6 (store a5 6 2))
-  (=> (and (<= 0 7) (< 7 20))
-  (forall ((a7 (Array Int Int)))
-  (=> (= a7 (store a6 7 1))
-  (=> (and (<= 0 8) (< 8 20))
-  (forall ((a8 (Array Int Int)))
-  (=> (= a8 (store a7 8 10))
-  (=> (and (<= 0 9) (< 9 20))
-  (forall ((a9 (Array Int Int)))
-  (=> (= a9 (store a8 9 6))
-  (=> (and (<= 0 10) (< 10 20))
-  (forall ((a10 (Array Int Int)))
-  (=> (= a10 (store a9 10 9))
-  (=> (and (<= 0 11) (< 11 20))
-  (forall ((a11 (Array Int Int)))
-  (=> (= a11 (store a10 11 5))
-  (=> (and (<= 0 12) (< 12 20))
-  (forall ((a12 (Array Int Int)))
-  (=> (= a12 (store a11 12 0))
-  (=> (and (<= 0 13) (< 13 20))
-  (forall ((a13 (Array Int Int)))
-  (=> (= a13 (store a12 13 2))
-  (=> (and (<= 0 14) (< 14 20))
-  (forall ((a14 (Array Int Int)))
-  (=> (= a14 (store a13 14 7))
-  (=> (and (<= 0 15) (< 15 20))
-  (forall ((a15 (Array Int Int)))
-  (=> (= a15 (store a14 15 3))
-  (=> (and (<= 0 16) (< 16 20))
-  (forall ((a16 (Array Int Int)))
-  (=> (= a16 (store a15 16 2))
-  (=> (and (<= 0 17) (< 17 20))
-  (forall ((a17 (Array Int Int)))
-  (=> (= a17 (store a16 17 1))
-  (=> (and (<= 0 18) (< 18 20))
-  (forall ((a18 (Array Int Int)))
-  (=> (= a18 (store a17 18 10))
-  (=> (and (<= 0 19) (< 19 20))
-  (forall ((a19 (Array Int Int)))
-  (=> (= a19 (store a18 19 6))
-  (=>
-  (and (<= 0 20)
-  (forall ((i Int)) (=> (and (<= 0 i) (< i 20)) (<= 0 (select a19 i)))))
-  (forall ((result Int) (result1 Int))
-  (=>
-  (and (= result (sum a19 0 20))
-  (and (is_max (mk_array1 20 a19) 0 20 result1) (<= result (* 20 result1))))
-  (= result 90)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-(check-sat)
-