Merge pull request #28 from kbansal/sets

Sets translator, bug fixes

17 files changed, 578 insertions, 31 deletions

diff --git a/examples/Makefile.am b/examples/Makefile.am
index 940af06ff..0f5c7db98 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -1,14 +1,16 @@
-SUBDIRS = nra-translate hashsmt api .
+SUBDIRS = nra-translate sets-translate hashsmt api .
 
 AM_CPPFLAGS = \
 	-I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall
 AM_CFLAGS = -Wall
 
+
 noinst_PROGRAMS = \
 	simple_vc_cxx \
 	translator
 
+
 if CVC4_BUILD_LIBCOMPAT
 noinst_PROGRAMS += \
 	simple_vc_compat_cxx
diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am
index 0d0236376..3508f9900 100644
--- a/examples/api/Makefile.am
+++ b/examples/api/Makefile.am
@@ -32,6 +32,8 @@ combination_LDADD = \
 
 helloworld_SOURCES = \
 	helloworld.cpp
+helloworld_CXXFLAGS = \
+	-DCVC4_MAKE_EXAMPLES
 helloworld_LDADD = \
 	@builddir@/../../src/libcvc4.la
 
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index b74f229b6..4c62874b8 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -15,9 +15,13 @@
  **/
 
 #include <iostream>
-#warning "To use helloworld.cpp as given in the wiki, instead of make examples, change the following two includes lines."
+
+#ifdef CVC4_MAKE_EXAMPLES
 #include "smt/smt_engine.h" // for use with make examples
-//#include <cvc4/cvc4.h> // To follow the wiki
+#else
+#include <cvc4/cvc4.h>      // To follow the wiki
+#endif /* CVC4_MAKE_EXAMPLES */
+
 using namespace CVC4;
 int main() {
   ExprManager em;
diff --git a/examples/sets-translate/Makefile b/examples/sets-translate/Makefile
new file mode 100644
index 000000000..8efe0c48e
--- /dev/null
+++ b/examples/sets-translate/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = examples/sets-translate
+
+include $(topdir)/Makefile.subdir
diff --git a/examples/sets-translate/Makefile.am b/examples/sets-translate/Makefile.am
new file mode 100644
index 000000000..40b79e998
--- /dev/null
+++ b/examples/sets-translate/Makefile.am
@@ -0,0 +1,19 @@
+AM_CPPFLAGS = \
+	-I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES)
+AM_CXXFLAGS = -Wall
+AM_CFLAGS = -Wall
+
+noinst_PROGRAMS = \
+	sets_translate	
+
+noinst_DATA =
+
+sets_translate_SOURCES = \
+	sets_translate.cpp
+sets_translate_LDADD = \
+	@builddir@/../../src/parser/libcvc4parser.la \
+	@builddir@/../../src/libcvc4.la
+
+# for installation
+examplesdir = $(docdir)/$(subdir)
+examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
new file mode 100644
index 000000000..6cf2b61e2
--- /dev/null
+++ b/examples/sets-translate/sets_translate.cpp
@@ -0,0 +1,286 @@
+/*********************                                                        */
+/*! \file sets-translate.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: None
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <string>
+#include <iostream>
+#include <typeinfo>
+#include <cassert>
+#include <vector>
+
+
+#include "options/options.h"
+#include "expr/expr.h"
+#include "theory/logic_info.h"
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::options;
+
+bool nonsense(char c) { return !isalnum(c); } 
+
+class Mapper {
+  set< Type > setTypes;
+  map< Type, Type > mapTypes;
+  map< pair<Type, Kind>, Expr > setoperators;
+  hash_map< Expr, Expr, ExprHashFunction > substitutions;
+  ostringstream sout;
+  ExprManager* em;
+
+  Expr add(SetType t, Expr e) {
+
+    if(setTypes.find(t) == setTypes.end() ) {
+      // mark as processed
+      setTypes.insert(t);
+
+      Type elementType = t.getElementType();
+      string elementTypeAsString = elementType.toString();
+      remove_if(elementTypeAsString.begin(), elementTypeAsString.end(), nonsense);
+
+      // define-sort
+      ostringstream oss_name;
+      oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2)
+               << "(Set " << elementType << ")";
+      string name = oss_name.str();
+      Type newt = em->mkArrayType(t.getElementType(), em->booleanType());
+      mapTypes[t] = newt;
+
+      // diffent types
+      vector<Type> t_t;
+      t_t.push_back(t);
+      t_t.push_back(t);
+      vector<Type> elet_t;
+      elet_t.push_back(elementType);
+      elet_t.push_back(t);
+
+      sout << "(define-fun emptyset" << elementTypeAsString << "    "
+           << " ()"
+           << " " << name
+           << " ( (as const " << name << ") false ) )" << endl;
+      setoperators[ make_pair(t, kind::EMPTYSET) ] =
+        em->mkVar( std::string("emptyset") + elementTypeAsString,
+                   t);
+
+      sout << "(define-fun setenum" << elementTypeAsString << "     "
+           << " ( (x " << elementType << ") )"
+           << " " << name << ""
+           << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
+      setoperators[ make_pair(t, kind::SET_SINGLETON) ] =
+        em->mkVar( std::string("setenum") + elementTypeAsString,
+                   em->mkFunctionType( elementType, t ) );
+
+      sout << "(define-fun union" << elementTypeAsString << "       "
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " " << name << ""
+           << " ((_ map or) s1 s2))" << endl;
+      setoperators[ make_pair(t, kind::UNION) ] =
+        em->mkVar( std::string("union") + elementTypeAsString,
+                   em->mkFunctionType( t_t, t ) );
+
+      sout << "(define-fun intersection" << elementTypeAsString << ""
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " " << name << ""
+           << " ((_ map and) s1 s2))" << endl;
+      setoperators[ make_pair(t, kind::INTERSECTION) ] =
+        em->mkVar( std::string("intersection") + elementTypeAsString,
+                   em->mkFunctionType( t_t, t ) );
+
+      sout << "(define-fun setminus" << elementTypeAsString << "    "
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " " << name << ""
+           << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl;
+      setoperators[ make_pair(t, kind::SETMINUS) ] =
+        em->mkVar( std::string("setminus") + elementTypeAsString,
+                   em->mkFunctionType( t_t, t ) );
+
+      sout << "(define-fun in" << elementTypeAsString << "          "
+           << " ( (x " << elementType << ")" << " (s " << name << "))"
+           << " Bool"
+           << " (select s x) )" << endl;
+      setoperators[ make_pair(t, kind::MEMBER) ] =
+        em->mkVar( std::string("in") + elementTypeAsString,
+                   em->mkPredicateType( elet_t ) );
+
+      sout << "(define-fun subseteq" << elementTypeAsString << "    "
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " Bool"
+           <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl;
+      setoperators[ make_pair(t, kind::SUBSET) ] =
+        em->mkVar( std::string("subseteq") + elementTypeAsString,
+                   em->mkPredicateType( t_t ) );
+
+    }
+    Expr ret;
+    if(e.getKind() == kind::EMPTYSET) {
+      ret = setoperators[ make_pair(t, e.getKind()) ];
+    } else {
+      vector<Expr> children = e.getChildren();
+      children.insert(children.begin(), setoperators[ make_pair(t, e.getKind()) ]);
+      ret = em->mkExpr(kind::APPLY, children);
+    }
+    // cout << "returning " << ret  << endl;
+    return ret;
+  }
+
+public:
+  Mapper(ExprManager* e) : em(e) {
+    sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+  }
+
+  void defineSetSort() {
+    if(setTypes.empty()) {
+      cout << "(define-sort Set (X) (Array X Bool) )" << endl;
+    }
+  }
+
+
+  Expr collectSortsExpr(Expr e)
+  {
+    Expr old_e = e;
+    for(unsigned i = 0; i < e.getNumChildren(); ++i) {
+      collectSortsExpr(e[i]);
+    }
+    e = e.substitute(substitutions);
+    if(theory::kindToTheoryId(e.getKind()) == theory::THEORY_SETS) {
+      SetType t = SetType(e.getType().isBoolean() ? e[1].getType() : e.getType());
+      substitutions[e] = add(t, e);
+      e = e.substitute(substitutions);
+    }
+    // cout << old_e << " => " << e << endl;
+    return e;
+  }
+
+  void dump() {
+    cout << sout.str();
+  }
+};
+
+
+int main(int argc, char* argv[]) 
+{
+
+  try {
+
+    // Get the filename 
+    string input;
+    if(argv > 0) input = (argv[1]);
+    else input = "<stdin>";
+
+    // Create the expression manager
+    Options options;
+    options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+    ExprManager exprManager(options);
+
+    Mapper m(&exprManager);
+  
+    // Create the parser
+    ParserBuilder parserBuilder(&exprManager, input, options);
+    Parser* parser = parserBuilder.build();
+  
+    // Variables and assertions
+    vector<string> variables;
+    vector<string> info_tags;
+    vector<string> info_data;
+    vector<Expr> assertions;
+  
+    Command* cmd = NULL;
+    CommandSequence commandsSequence;
+    bool logicisset = false;
+
+    while ((cmd = parser->nextCommand())) {
+
+      // till logic is set, don't do any modifications
+      if(!parser->logicIsSet()) {
+        cout << (*cmd) << endl;
+        delete cmd;
+        continue;
+      }
+
+      // transform set-logic command, if there is one
+      SetBenchmarkLogicCommand* setlogic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(setlogic) {
+	LogicInfo logicinfo(setlogic->getLogic());
+	if(!logicinfo.isTheoryEnabled(theory::THEORY_SETS)) {
+	  cerr << "Sets theory not enabled. Stopping translation." << endl;
+	  return 0;
+	}
+        logicinfo = logicinfo.getUnlockedCopy();
+        logicinfo.disableTheory(theory::THEORY_SETS);
+        logicinfo.enableTheory(theory::THEORY_ARRAY);
+        logicinfo.lock();
+        // cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl;
+
+        delete cmd;
+        continue;
+      }
+
+      // if we reach here, logic is set by now, so can define our sort
+      if( !logicisset ) {
+        logicisset = true;
+        m.defineSetSort();
+      }
+
+      // declare/define-sort commands are printed immediately
+      DeclareTypeCommand* declaresort = dynamic_cast<DeclareTypeCommand*>(cmd);
+      DefineTypeCommand* definesort = dynamic_cast<DefineTypeCommand*>(cmd);
+      if(declaresort || definesort) {
+        cout << *cmd << endl;
+        delete cmd;
+        continue;
+      }
+
+      // other commands are queued up, while replacing with new function symbols
+      AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
+      DeclareFunctionCommand* declarefun = dynamic_cast<DeclareFunctionCommand*>(cmd);
+      DefineFunctionCommand* definefun = dynamic_cast<DefineFunctionCommand*>(cmd);
+
+      Command* new_cmd = NULL;
+      if(assert) {
+        Expr newexpr = m.collectSortsExpr(assert->getExpr());
+        new_cmd = new AssertCommand(newexpr);
+      } else if(declarefun) {
+        Expr newfunc = m.collectSortsExpr(declarefun->getFunction());
+        new_cmd = new DeclareFunctionCommand(declarefun->getSymbol(), newfunc, declarefun->getType());
+      } else if(definefun) {
+        Expr newfunc = m.collectSortsExpr(definefun->getFunction());
+        Expr newformula = m.collectSortsExpr(definefun->getFormula());
+        new_cmd = new DefineFunctionCommand(definefun->getSymbol(), newfunc, definefun->getFormals(), newformula);
+      }
+
+      if(new_cmd == NULL) {
+        commandsSequence.addCommand(cmd);
+      } else {
+        commandsSequence.addCommand(new_cmd);
+        delete cmd;
+      }
+
+    }
+
+    m.dump();
+    cout << commandsSequence;
+    
+  
+    // Get rid of the parser
+    //delete parser;
+  } catch (Exception& e) {
+    cerr << e << endl;
+  }
+}
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 987feafac..d54aa3a83 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -333,8 +333,9 @@ function register_kind {
   r=$1
   nc=$2
   comment=$3
+  register_kind_counter=$[register_kind_counter+1]
 
-  kind_decls="${kind_decls}  $r, /**< $comment */
+  kind_decls="${kind_decls}  $r, /**< $comment ($register_kind_counter) */
 "
   kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
 "
diff --git a/src/expr/options b/src/expr/options
index cf893a7a5..ee4d40b2c 100644
--- a/src/expr/options
+++ b/src/expr/options
@@ -7,8 +7,13 @@ module EXPR "expr/options.h" Expression package
 
 option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
  print exprs to depth N (0 == default, -1 == no limit)
+undocumented-alias --expr-depth = --default-expr-depth
+
 option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h"
  dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
+undocumented-alias --dag-thresh = --default-dag-thresh
+undocumented-alias --dag-threshold = --default-dag-thresh
+
 option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
  print types with variables when printing exprs
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 60b99132d..4c33088d4 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -85,6 +85,35 @@ void printUsage(Options& opts, bool full) {
   }
 }
 
+void printStatsFilterZeros(std::ostream& out, const std::string& statsString) {
+  // read each line, if a number, check zero and skip if so
+  // Stat are assumed to one-per line: "<statName>, <statValue>"
+
+  std::istringstream iss(statsString);
+  std::string statName, statValue;
+
+  std::getline(iss, statName, ',');
+
+  while( !iss.eof() ) {
+
+    std::getline(iss, statValue, '\n');
+
+    double curFloat;
+    bool isFloat = (std::istringstream(statValue) >> curFloat);
+
+    if( (isFloat && curFloat == 0) ||
+        statValue == " \"0\"" ||
+        statValue == " \"[]\"") {
+      // skip
+    } else {
+      out << statName << "," << statValue << std::endl;
+    }
+
+    std::getline(iss, statName, ',');
+  }
+
+}
+
 int runCvc4(int argc, char* argv[], Options& opts) {
 
   // Timer statistic
@@ -419,7 +448,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     // Set the global executor pointer to NULL first.  If we get a
     // signal while dumping statistics, we don't want to try again.
     if(opts[options::statistics]) {
-      pExecutor->flushStatistics(*opts[options::err]);
+      if(opts[options::statsHideZeros] == false) {
+        pExecutor->flushStatistics(*opts[options::err]);
+      } else {
+        std::ostringstream ossStats;
+        pExecutor->flushStatistics(ossStats);
+        printStatsFilterZeros(*opts[options::err], ossStats.str());
+      }
     }
 
     // make sure to flush replay output log before early-exit
diff --git a/src/options/base_options b/src/options/base_options
index f3ba38a6a..ed94e68f6 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -111,6 +111,11 @@ option statsEveryQuery --stats-every-query bool :default false :link --stats
  in incremental mode, print stats after every satisfiability or validity query
 undocumented-alias --statistics-every-query = --stats-every-query
 undocumented-alias --no-statistics-every-query = --no-stats-every-query
+option statsHideZeros --stats-hide-zeros/--stats-show-zeros bool :default false
+ hide statistics which are zero
+/show statistics even when they are zero (default)
+undocumented-alias --hide-zero-stats = --stats-hide-zeros
+undocumented-alias --show-zero-stats = --stats-show-zeros
 
 option parseOnly parse-only --parse-only bool :read-write
  exit after parsing input
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 15813a774..e701ee13d 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -121,6 +121,18 @@ inline std::string suggestTags(char const* const* validTags, std::string inputTa
 inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) {
   if(Configuration::isTracingBuild()) {
     if(!Configuration::isTraceTag(optarg.c_str()))
+
+      if(optarg == "help") {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumTraceTags();
+        char const* const* tags = Configuration::getTraceTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+        exit(0);
+      }
+
       throw OptionException(std::string("trace tag ") + optarg +
                             std::string(" not available.") +
                             suggestTags(Configuration::getTraceTags(), optarg) );
@@ -134,6 +146,18 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt)
   if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
     if(!Configuration::isDebugTag(optarg.c_str()) &&
        !Configuration::isTraceTag(optarg.c_str())) {
+
+      if(optarg == "help") {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumDebugTags();
+        char const* const* tags = Configuration::getDebugTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+        exit(0);
+      }
+
       throw OptionException(std::string("debug tag ") + optarg +
                             std::string(" not available.") +
                             suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) );
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 3f5e66492..2f30460d2 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -272,6 +272,10 @@ public:
   void disallowIncludeFile() { d_canIncludeFile = false; }
   bool canIncludeFile() const { return d_canIncludeFile; }
 
+  /** Expose the functionality from SMT/SMT2 parsers, while making
+      implementation optional by returning false by default. */
+  virtual bool logicIsSet() { return false; }
+
   void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; }
   const std::string& getForcedLogic() const { return d_forcedLogic; }
   bool logicIsForced() const { return d_logicIsForced; }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8201c9b7c..8e5a9dae4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -713,7 +713,7 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
 
 // SMT-LIB quoting for symbols
 static std::string quoteSymbol(std::string s) {
-  if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@%^&*_-+=<>.?/") == std::string::npos) {
+  if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") == std::string::npos) {
     // simple unquoted symbol
     return s;
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9ac1e9db..33496ac3b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3444,7 +3444,8 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   Trace("smt") << "--- model-post expected " << expectedType << endl;
 
   // type-check the result we got
-  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType));
+  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType),
+         "Run with -t smt for details.");
 
   // ensure it's a constant
   Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8c9441483..9b628ede2 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -990,6 +990,7 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, T
   if(value) {
     d_theory.d_termInfoManager->mergeTerms(t1, t2);
   }
+  d_theory.propagate( value ? EQUAL(t1, t2) : NOT(EQUAL(t1, t2)) );
   return true;
 }
 
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 7f1f07461..07006d6c3 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -19,49 +19,46 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	union-1b-flip.smt2 \
-	sets-sharing.smt2 \
-	union-1a-flip.smt2 \
-	copy_check_heap_access_33_4.smt2 \
-	rec_copy_loop_check_heap_access_43_4.smt2 \
-	sets-testlemma.smt2 \
 	jan24/insert_invariant_37_2.smt2 \
 	jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \
 	jan24/deepmeas0.hs.fqout.small.smt2 \
 	jan24/remove_check_free_31_6.smt2 \
-	sets-inter.smt2 \
-	sets-equal.smt2 \
-	sets-disequal.smt2 \
-	union-2.smt2 \
 	jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \
 	jan27/ListConcat.hs.fqout.cvc4.177.smt2 \
 	jan27/ListConcat.hs.fqout.177minimized.smt2 \
 	jan27/ListElem.hs.fqout.cvc4.38.smt2 \
-	feb3/ListElts.hs.fqout.cvc4.317.smt2 \
-	setel-eq.smt2 \
-	sets-new.smt2 \
+	jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
+	jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
 	jan30/UniqueZipper.hs.fqout.minimized10.smt2 \
 	jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 \
 	jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \
 	jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 \
-	emptyset.smt2 \
-	sets-union.smt2 \
-	error2.smt2 \
-	union-1b.smt2 \
-	union-1a.smt2 \
-	error1.smt2 \
-	jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
-	jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
-	sets-sample.smt2 \
-	eqtest.smt2 \
+	feb3/ListElts.hs.fqout.cvc4.317.smt2 \
 	mar2014/lemmabug-ListElts317minimized.smt2 \
 	mar2014/sharing-preregister.smt2 \
 	mar2014/small.smt2 \
 	mar2014/smaller.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
+	copy_check_heap_access_33_4.smt2 \
 	emptyset.smt2 \
-	error2.smt2
+	error1.smt2 \
+	error2.smt2 \
+	eqtest.smt2 \
+	rec_copy_loop_check_heap_access_43_4.smt2 \
+	sets-disequal.smt2 \
+	sets-equal.smt2 \
+	sets-inter.smt2 \
+	sets-sample.smt2 \
+	sets-sharing.smt2 \
+	sets-testlemma.smt2 \
+	sets-union.smt2 \
+	sharingbug.smt2 \
+	union-1a-flip.smt2 \
+	union-1a.smt2 \
+	union-1b-flip.smt2 \
+	union-1b.smt2 \
+	union-2.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2
new file mode 100644
index 000000000..b2b61f739
--- /dev/null
+++ b/test/regress/regress0/sets/sharingbug.smt2
@@ -0,0 +1,157 @@
+(set-info :source |fuzzsmt|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status sat)
+(set-logic QF_UFLIA_SETS)
+(define-sort Element () Int)
+(declare-fun f0 ( Int Int Int) Int)
+(declare-fun f1 ( (Set Element)) (Set Element))
+(declare-fun p0 ( Int Int Int) Bool)
+(declare-fun p1 ( (Set Element)) Bool)
+(declare-fun v0 () Int)
+(declare-fun v1 () (Set Element))
+(declare-fun v2 () (Set Element))
+(declare-fun v3 () (Set Element))
+(assert (let ((e4 1))
+(let ((e5 (- v0)))
+(let ((e6 (* v0 (- e4))))
+(let ((e7 (ite (p0 v0 e5 v0) 1 0)))
+(let ((e8 (- e6 e7)))
+(let ((e9 (+ e5 v0)))
+(let ((e10 (ite (p0 e7 e7 e5) 1 0)))
+(let ((e11 (+ e8 e10)))
+(let ((e12 (* (- e4) e7)))
+(let ((e13 (- e10)))
+(let ((e14 (f0 e5 e7 e6)))
+(let ((e15 (in v0 v1)))
+(let ((e16 (in e12 v2)))
+(let ((e17 (in e14 v1)))
+(let ((e18 (f1 v3)))
+(let ((e19 (f1 v2)))
+(let ((e20 (f1 v1)))
+(let ((e21 (>= v0 e9)))
+(let ((e22 (> e6 e6)))
+(let ((e23 (> e5 e12)))
+(let ((e24 (distinct e8 e11)))
+(let ((e25 (= e10 e10)))
+(let ((e26 (> e13 e13)))
+(let ((e27 (distinct e14 e10)))
+(let ((e28 (> e11 e5)))
+(let ((e29 (>= e14 e6)))
+(let ((e30 (< e14 e14)))
+(let ((e31 (< e7 e12)))
+(let ((e32 (<= e11 e12)))
+(let ((e33 (< e14 e11)))
+(let ((e34 (<= e7 e9)))
+(let ((e35 (distinct e12 e5)))
+(let ((e36 (= e14 e6)))
+(let ((e37 (< v0 e8)))
+(let ((e38 (< e13 e14)))
+(let ((e39 (>= e6 e13)))
+(let ((e40 (< e12 e13)))
+(let ((e41 (< v0 e14)))
+(let ((e42 (< v0 e11)))
+(let ((e43 (p0 e13 e7 e8)))
+(let ((e44 (ite e17 e19 e19)))
+(let ((e45 (ite e34 v1 v1)))
+(let ((e46 (ite e28 v1 e44)))
+(let ((e47 (ite e24 e44 e20)))
+(let ((e48 (ite e39 e18 v3)))
+(let ((e49 (ite e35 v2 v3)))
+(let ((e50 (ite e38 e18 e20)))
+(let ((e51 (ite e22 v2 e44)))
+(let ((e52 (ite e17 e20 e18)))
+(let ((e53 (ite e35 e52 e19)))
+(let ((e54 (ite e38 e49 e20)))
+(let ((e55 (ite e15 e20 e45)))
+(let ((e56 (ite e37 v1 v3)))
+(let ((e57 (ite e41 e50 v1)))
+(let ((e58 (ite e28 v1 e54)))
+(let ((e59 (ite e27 e19 e53)))
+(let ((e60 (ite e16 e46 e44)))
+(let ((e61 (ite e29 e57 e52)))
+(let ((e62 (ite e21 e50 e53)))
+(let ((e63 (ite e32 e45 e19)))
+(let ((e64 (ite e42 v3 e57)))
+(let ((e65 (ite e33 e50 v3)))
+(let ((e66 (ite e43 e49 e20)))
+(let ((e67 (ite e22 v1 e63)))
+(let ((e68 (ite e40 e45 e19)))
+(let ((e69 (ite e30 e62 e58)))
+(let ((e70 (ite e24 e52 e58)))
+(let ((e71 (ite e31 e64 e67)))
+(let ((e72 (ite e30 e18 e20)))
+(let ((e73 (ite e25 e58 e44)))
+(let ((e74 (ite e36 e63 v3)))
+(let ((e75 (ite e43 e62 e73)))
+(let ((e76 (ite e26 e61 e55)))
+(let ((e77 (ite e23 e61 e71)))
+(let ((e78 (ite e40 e13 v0)))
+(let ((e79 (ite e23 e8 e13)))
+(let ((e80 (ite e24 e78 e6)))
+(let ((e81 (ite e39 e9 e80)))
+(let ((e82 (ite e31 e7 v0)))
+(let ((e83 (ite e43 e14 e6)))
+(let ((e84 (ite e38 e80 e81)))
+(let ((e85 (ite e32 e14 e10)))
+(let ((e86 (ite e29 e84 e78)))
+(let ((e87 (ite e27 e12 e8)))
+(let ((e88 (ite e31 e11 e6)))
+(let ((e89 (ite e33 e88 e85)))
+(let ((e90 (ite e36 e12 v0)))
+(let ((e91 (ite e23 e5 e7)))
+(let ((e92 (ite e34 e89 e80)))
+(let ((e93 (ite e15 e79 v0)))
+(let ((e94 (ite e21 e6 e7)))
+(let ((e95 (ite e26 v0 e91)))
+(let ((e96 (ite e28 e94 e87)))
+(let ((e97 (ite e32 e90 e78)))
+(let ((e98 (ite e42 e78 e83)))
+(let ((e99 (ite e40 e13 e82)))
+(let ((e100 (ite e25 e88 e90)))
+(let ((e101 (ite e26 e11 e81)))
+(let ((e102 (ite e17 e101 e81)))
+(let ((e103 (ite e30 v0 e80)))
+(let ((e104 (ite e28 e80 e79)))
+(let ((e105 (ite e27 e95 e101)))
+(let ((e106 (ite e22 e92 e94)))
+(let ((e107 (ite e16 e82 e94)))
+(let ((e108 (ite e41 e10 e78)))
+(let ((e109 (ite e37 e107 e84)))
+(let ((e110 (ite e35 e89 e92)))
+(let ((e111 (and e30 e37)))
+(let ((e112 (=> e21 e41)))
+(let ((e113 (ite e25 e33 e26)))
+(let ((e114 (and e34 e38)))
+(let ((e115 (=> e22 e43)))
+(let ((e116 (and e24 e35)))
+(let ((e117 (not e112)))
+(let ((e118 (=> e27 e116)))
+(let ((e119 (= e36 e15)))
+(let ((e120 (= e42 e42)))
+(let ((e121 (xor e29 e115)))
+(let ((e122 (xor e39 e16)))
+(let ((e123 (or e118 e32)))
+(let ((e124 (not e28)))
+(let ((e125 (=> e23 e40)))
+(let ((e126 (ite e17 e123 e111)))
+(let ((e127 (not e117)))
+(let ((e128 (not e31)))
+(let ((e129 (xor e121 e126)))
+(let ((e130 (or e125 e119)))
+(let ((e131 (=> e127 e114)))
+(let ((e132 (or e113 e128)))
+(let ((e133 (= e122 e124)))
+(let ((e134 (not e130)))
+(let ((e135 (or e133 e132)))
+(let ((e136 (= e129 e135)))
+(let ((e137 (=> e120 e120)))
+(let ((e138 (or e134 e137)))
+(let ((e139 (or e138 e138)))
+(let ((e140 (and e139 e131)))
+(let ((e141 (or e136 e136)))
+(let ((e142 (= e140 e141)))
+e142
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+(check-sat)