Added preprocessing pass that propagates unconstrained values - solves all of

the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

diff --git a/src/expr/node.h b/src/expr/node.h
index 4d39ec60f4b518290a45fdc52b9697fbc089afd4..3532116bcdabab54ba1b55a3a3cb977f3b7b5485 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -450,6 +450,15 @@ public:
     return getMetaKind() == kind::metakind::CONSTANT;
   }
 
+  /**
+   * Returns true if this node represents a constant
+   * @return true if const
+   */
+  inline bool isVar() const {
+    assertTNodeNotExpired();
+    return getMetaKind() == kind::metakind::VARIABLE;
+  }
+
   /**
    * Returns the unique id of this node
    * @return the ud

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index ade887b23ec0e0bb7c0c92bf67df59b364927c11..b9db8daced356e52401736428969b212565bb263 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -49,6 +49,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFNRA"] = QF_UFNRA;
   logicMap["QF_ABV"] = QF_ABV;
   logicMap["QF_AUFBV"] = QF_AUFBV;
+  logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
+  logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
@@ -219,6 +221,20 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case QF_AUFBVLIA:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFBVLRA:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
   case QF_AUFLIA:
     addTheory(THEORY_INT_ARRAYS_EX);
     addUf();

diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 1606d7baba98a557737b089b717a23ceca8300ec..34ec624bc28a497c7fc5c9dc8c7a3205bce19f2b 100644 (file)
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -42,6 +42,8 @@ public:
     LRA,
     QF_ABV,
     QF_AUFBV,
+    QF_AUFBVLIA,
+    QF_AUFBVLRA,
     QF_AUFLIA,
     QF_AUFLIRA,
     QF_AX,

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index dc1b47bdef1d5364b9c087b0994715a5f1fda18d..3fa00baaecf82d469dacb2ba4ec4adae9ca33327 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,20 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_AUFBVLIA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case Smt::QF_AUFBVLRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
   case Smt::QF_AUFLIA:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 68485ca8ada98a267e58c3c0e6cd78d7e0f6e73c..14b3e3b42831c9d3fc51a2bbc6df20b367032089 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -159,6 +159,9 @@ class SmtEnginePrivate {
   // Simplify ITE structure
   void simpITE();
 
+  // Simplify based on unconstrained values
+  void unconstrainedSimp();
+
   /**
    * Any variable in a assertion that is declared as a subtype type
    * (predicate subtype or integer subrange type) must be constrained
@@ -255,6 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
   d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
   d_simpITETime("smt::SmtEngine::simpITETime"),
+  d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
   d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
   d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
   d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
@@ -268,6 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
   StatisticsRegistry::registerStat(&d_staticLearningTime);
   StatisticsRegistry::registerStat(&d_simpITETime);
+  StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
   StatisticsRegistry::registerStat(&d_iteRemovalTime);
   StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
   StatisticsRegistry::registerStat(&d_cnfConversionTime);
@@ -373,6 +378,7 @@ SmtEngine::~SmtEngine() throw() {
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
     StatisticsRegistry::unregisterStat(&d_simpITETime);
+    StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
     StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
     StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
     StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
@@ -449,6 +455,13 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
     NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
   }
+  // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
+  if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
+    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+    bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
+    Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
+    NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
+  }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! Options::current()->arithRewriteEqSetByUser) {
     bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
@@ -886,16 +899,24 @@ void SmtEnginePrivate::nonClausalSimplify() {
     d_nonClausalLearnedLiterals.resize(j);
   }
 
+  hash_set<TNode, TNodeHashFunction> s;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])));
+    Node assertion = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
+    s.insert(assertion);
+    d_assertionsToCheck.push_back(assertion);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "non-clausal preprocessed: "
-                      << d_assertionsToCheck.back() << endl;
+                      << assertion << endl;
   }
   d_assertionsToPreprocess.clear();
 
   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
-    d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i])));
+    Node learned = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]));
+    if (s.find(learned) != s.end()) {
+      continue;
+    }
+    s.insert(learned);
+    d_assertionsToCheck.push_back(learned);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "non-clausal learned : "
                       << d_assertionsToCheck.back() << endl;
@@ -916,6 +937,16 @@ void SmtEnginePrivate::simpITE()
   }
 }
 
+
+void SmtEnginePrivate::unconstrainedSimp()
+{
+  TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_unconstrainedSimpTime);
+
+  Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
+  d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck);
+}
+
+
 void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
   throw(AssertionException) {
 
@@ -993,7 +1024,10 @@ void SmtEnginePrivate::simplifyAssertions()
       // Perform non-clausal simplification
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << "performing non-clausal simplification" << endl;
+      // Abuse the user context to make sure circuit propagator gets backtracked
+      d_smt.d_userContext->push();
       nonClausalSimplify();
+      d_smt.d_userContext->pop();
     } else {
       Assert(d_assertionsToCheck.empty());
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
@@ -1004,9 +1038,16 @@ void SmtEnginePrivate::simplifyAssertions()
       simpITE();
     }
 
+    if(Options::current()->unconstrainedSimp) {
+      unconstrainedSimp();
+    }
+
     if(Options::current()->repeatSimp) {
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
+      // Abuse the user context to make sure circuit propagator gets backtracked
+      d_smt.d_userContext->push();
       nonClausalSimplify();
+      d_smt.d_userContext->pop();
     }
 
     if(Options::current()->doStaticLearning) {

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 10a37b712ac07099a00da64967e9cbac830e39ae..f07815e2e73331376b51c871125629701939c720 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -231,6 +231,8 @@ class CVC4_PUBLIC SmtEngine {
   TimerStat d_staticLearningTime;
   /** time spent in simplifying ITEs */
   TimerStat d_simpITETime;
+  /** time spent in simplifying ITEs */
+  TimerStat d_unconstrainedSimpTime;
   /** time spent removing ITEs */
   TimerStat d_iteRemovalTime;
   /** time spent in theory preprocessing */

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 1341c048abfac4b9f57b783989ba17f7750ac21b..85d6fbdf88d4cd6596bb145fb9c01ed6e7c54c8e 100644 (file)
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -31,7 +31,9 @@ libtheory_la_SOURCES = \
        term_registration_visitor.h \
        term_registration_visitor.cpp \
        ite_simplifier.h \
-       ite_simplifier.cpp
+       ite_simplifier.cpp \
+       unconstrained_simplifier.h \
+       unconstrained_simplifier.cpp
 
 nodist_libtheory_la_SOURCES = \
        rewriter_tables.h \

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index f5e4f4630d3fdfb9abcdb583e5069acb2db1d54f..60e48dba22f0a3a92ed1afc01188783fdb01844a 100644 (file)
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -68,10 +68,6 @@ public:
 
 private:
 
-  /** Back edges from nodes to where they are used */
-  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
-  BackEdgesMap d_backEdges;
-
   /** The propagation queue */
   std::vector<TNode> d_propagationQueue;
 
@@ -111,6 +107,15 @@ private:
    */
   DataClearer< std::vector<Node> > d_learnedLiteralClearer;
 
+  /** Back edges from nodes to where they are used */
+  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+  BackEdgesMap d_backEdges;
+
+  /**
+   * Similar data clearer for back edges.
+   */
+  DataClearer<BackEdgesMap> d_backEdgesClearer;
+
   /** Nodes that have been attached already (computed forward edges for) */
   // All the nodes we've visited so far
   context::CDHashSet<TNode, TNodeHashFunction> d_seen;
@@ -231,12 +236,13 @@ public:
    */
   CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals,
                     bool enableForward = true, bool enableBackward = true) :
-    d_backEdges(),
     d_propagationQueue(),
     d_propagationQueueClearer(context, d_propagationQueue),
     d_conflict(context, false),
     d_learnedLiterals(outLearnedLiterals),
     d_learnedLiteralClearer(context, outLearnedLiterals),
+    d_backEdges(),
+    d_backEdgesClearer(context, d_backEdges),
     d_seen(context),
     d_state(context),
     d_forwardPropagation(enableForward),

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 5be0529474ecf689002135a10a468d4f33af3202..197134b6a1983b314a623a65d27782c66e840a85 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -405,6 +405,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
       updateCoefMap(left[i], size, leftMap, leftConst);
     }
   }
+  else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right) {
+    return utils::mkFalse();
+  }
   else {
     updateCoefMap(left, size, leftMap, leftConst);
   }
@@ -415,6 +418,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
       updateCoefMap(right[i], size, rightMap, rightConst);
     }
   }
+  else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left) {
+    return utils::mkFalse();
+  }
   else {
     updateCoefMap(right, size, rightMap, rightConst);
   }

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index caf7566b913016e4638f21c23c74448d4d385b40..b7ad1d174e977315fafb97f41298b90e320e8387 100644 (file)
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -71,6 +71,10 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache)
       }
       // Mark the substitution and continue
       Node result = builder;
+      find = substitutionCache.find(result);
+      if (find != substitutionCache.end()) {
+        result = find->second;
+      }
       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
       substitutionCache[current] = result;
       toVisit.pop_back();
@@ -114,13 +118,16 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
     d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
   }
 
-  // Put the new substitution in
-  d_substitutions[x] = t;
+  // Put the new substitution in, but apply existing substitutions to rhs first
+  d_substitutions[x] = apply(t);
 
   // Also invalidate the cache
   if (invalidateCache) {
     d_cacheInvalidated = true;
   }
+  else {
+    d_substitutionCache[x] = d_substitutions[x];
+  }
 }
 
 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 958f502762f0d4f1454fe5fadda306433deb211f..711ff9b72d0af4ffa8ce1174a5478c991431f68e 100644 (file)
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -106,6 +106,12 @@ public:
    */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 
+  /**
+   * Returns true iff x is in the substitution map
+   */
+  bool hasSubstitution(TNode x)
+    { return d_substitutions.find(x) != d_substitutions.end(); }
+
   /**
    * Apply the substitutions to the node.
    */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f72275cb21aa593da0542219c3f27c975b2a10b5..4ed0bcb60461e04a84271495cdb0bacb106583ac 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -62,7 +62,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_inPreregister(false),
   d_preRegistrationVisitor(this, context),
-  d_sharedTermsVisitor(d_sharedTerms)
+  d_sharedTermsVisitor(d_sharedTerms),
+  d_unconstrainedSimp(context, logicInfo)
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     d_theoryTable[theoryId] = NULL;
@@ -1011,3 +1012,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion)
   result = Rewriter::rewrite(result);
   return result;
 }
+
+
+void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
+{
+  d_unconstrainedSimp.processAssertions(assertions);
+}

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 019818a5f7ce0099d8e22e1f11d350ee36c05b88..bc9f4c8895b1e0c82c2bf9e9f6edac80e5415d65 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -42,6 +42,7 @@
 #include "util/hash.h"
 #include "util/cache.h"
 #include "theory/ite_simplifier.h"
+#include "theory/unconstrained_simplifier.h"
 
 namespace CVC4 {
 
@@ -734,8 +735,12 @@ private:
   /** For preprocessing pass simplifying ITEs */
   ITESimplifier d_iteSimplifier;
 
+  /** For preprocessing pass simplifying unconstrained expressions */
+  UnconstrainedSimplifier d_unconstrainedSimp;
+
 public:
   Node ppSimpITE(TNode assertion);
+  void ppUnconstrainedSimp(std::vector<Node>& assertions);
 
 };/* class TheoryEngine */
 

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 01b9648ffbb46337d48bf62c6a145217aea25389..e9ef7d959bb9c65e166a0a3ad0413e9982b3da06 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -85,6 +85,8 @@ Options::Options() :
   doStaticLearning(true),
   doITESimp(false),
   doITESimpSetByUser(false),
+  unconstrainedSimp(false),
+  unconstrainedSimpSetByUser(false),
   repeatSimp(false),
   repeatSimpSetByUser(false),
   interactive(false),
@@ -189,6 +191,8 @@ Additional CVC4 options:\n\
    --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
    --ite-simp             turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
    --no-ite-simp          turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
+   --unconstrained-simp   turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
+   --no-unconstrained-simp turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
    --repeat-simp          make multiple passes with nonclausal simplifier\n\
    --no-repeat-simp       do not make multiple passes with nonclausal simplifier\n\
    --replay=file          replay decisions from file\n\
@@ -430,6 +434,8 @@ enum OptionValue {
   NO_STATIC_LEARNING,
   ITE_SIMP,
   NO_ITE_SIMP,
+  UNCONSTRAINED_SIMP,
+  NO_UNCONSTRAINED_SIMP,
   REPEAT_SIMP,
   NO_REPEAT_SIMP,
   INTERACTIVE,
@@ -530,6 +536,8 @@ static struct option cmdlineOptions[] = {
   { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
   { "ite-simp", no_argument, NULL, ITE_SIMP },
   { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
+  { "unconstrained-simp", no_argument, NULL, UNCONSTRAINED_SIMP },
+  { "no-unconstrained-simp", no_argument, NULL, NO_UNCONSTRAINED_SIMP },
   { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
   { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
   { "interactive", no_argument      , NULL, INTERACTIVE },
@@ -855,6 +863,16 @@ throw(OptionException) {
       doITESimpSetByUser = true;
       break;
 
+    case UNCONSTRAINED_SIMP:
+      unconstrainedSimp = true;
+      unconstrainedSimpSetByUser = true;
+      break;
+
+    case NO_UNCONSTRAINED_SIMP:
+      unconstrainedSimp = false;
+      unconstrainedSimpSetByUser = true;
+      break;
+
     case REPEAT_SIMP:
       repeatSimp = true;
       repeatSimpSetByUser = true;

diff --git a/src/util/options.h b/src/util/options.h
index e6135dacbda3739385c3986b4d1850c417960c16..f48b45b49cb7b095c41addd095a8f20bf3af293b 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options {
    */
   bool doITESimpSetByUser;
 
+  /** Whether to do the unconstrained simplification pass */
+  bool unconstrainedSimp;
+
+  /**
+   * Whether the user explicitly requested unconstrained simplification
+   */
+  bool unconstrainedSimpSetByUser;
+
   /** Whether to do multiple rounds of nonclausal simplification */
   bool repeatSimp;
 

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
new file mode 100644 (file)
index 0000000..241b788
--- /dev/null
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -0,0 +1,78 @@
+BINARY = cvc4
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
+else
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =        \
+       arith2.smt2 \
+       arith3.smt2 \
+       arith4.smt2 \
+       arith5.smt2 \
+       arith6.smt2 \
+       arith7.smt2 \
+       arith.smt2 \
+       array1.smt2 \
+       bvbool2.smt2 \
+       bvbool3.smt2 \
+       bvbool.smt2 \
+       bvcmp.smt2 \
+       bvconcat2.smt2 \
+       bvconcat.smt2 \
+       bvdiv2.smt2 \
+       bvdiv.smt2 \
+       bvext.smt2 \
+       bvite.smt2 \
+       bvmul2.smt2 \
+       bvmul3.smt2 \
+       bvmul.smt2 \
+       bvnot.smt2 \
+       bvsle2.smt2 \
+       bvsle3.smt2 \
+       bvsle4.smt2 \
+       bvsle5.smt2 \
+       bvsle.smt2 \
+       bvslt2.smt2 \
+       bvslt3.smt2 \
+       bvslt4.smt2 \
+       bvslt5.smt2 \
+       bvslt.smt2 \
+       bvule2.smt2 \
+       bvule3.smt2 \
+       bvule4.smt2 \
+       bvule5.smt2 \
+       bvule.smt2 \
+       bvult2.smt2 \
+       bvult3.smt2 \
+       bvult4.smt2 \
+       bvult5.smt2 \
+       bvult.smt2 \
+       geq.smt2 \
+       gt.smt2 \
+       leq.smt2 \
+       lt.smt2 \
+       uf1.smt2 \
+       uf2.smt2 \
+       xor.smt2
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#      error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#      error.cvc
+
+# synonyms for "check" in this directory
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:

diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2
new file mode 100644 (file)
index 0000000..dc2b274
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (< v2 100))
+(assert (not (= (a2 (- (+ v1 5) v2)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2
new file mode 100644 (file)
index 0000000..f9e829e
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith2.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun v3 () Real)
+(assert (= (+ v1 v2) v3))
+(assert (< v3 v2))
+(assert (> v3 (- v2 1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2
new file mode 100644 (file)
index 0000000..83634a5
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith3.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun v3 () Int)
+(declare-fun v4 () Int)
+(assert (= (* v1 v2) v3))
+(assert (< v3 v4))
+(assert (> v3 (- v4 1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2
new file mode 100644 (file)
index 0000000..8cb825a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith4.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun v3 () Int)
+(declare-fun v4 () Int)
+(declare-fun v5 () Real)
+(assert (= (* v1 v2) (+ (* v3 v4) v5)))
+(assert (< v5 1))
+(assert (> v5 0))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2
new file mode 100644 (file)
index 0000000..de1e305
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith5.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Real)
+(declare-fun a2 (Real) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (* 2 v1)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2
new file mode 100644 (file)
index 0000000..0565341
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith6.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Real)
+(declare-fun a2 (Real) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (/ v1 2)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2
new file mode 100644 (file)
index 0000000..6cc063c
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith7.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Real)
+(assert (= (/ v1 2) v2))
+(assert (< v2 (/ 1 2)))
+(assert (> v2 0))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2
new file mode 100644 (file)
index 0000000..82f084e
--- /dev/null
+++ b/test/regress/regress0/unconstrained/array1.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun a2 () (Array (_ BitVec 16) (_ BitVec 1024)))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (select a2 v1) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2
new file mode 100644 (file)
index 0000000..0dded2a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2
new file mode 100644 (file)
index 0000000..9490962
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool2.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (= (bvand x0 x1) ((_ extract 9 0) v3)))
+(assert (= x1 (_ bv0 10)))
+(assert (= v3 (_ bv1 1024)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2
new file mode 100644 (file)
index 0000000..6f72246
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool3.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (=> (or p1 p1) (and (= (bvnor (bvnand (bvor x1 x1) (bvand x0 x0)) x3) ((_ extract 9 0) v3)) p1))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvbool3.smt3 b/test/regress/regress0/unconstrained/bvbool3.smt3
new file mode 100644 (file)
index 0000000..7c93626
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool3.smt3
@@ -0,0 +1,37 @@
+(set-logic QF_AUFBVLIA)
+(set-info :source |
+This benchmark demonstrates the need for propagating unconstrained arrays
+and bit-vectors.
+
+Contributed by Robert Brummayer (robert.brummayer@gmail.com)
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2
new file mode 100644 (file)
index 0000000..ba73163
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvcmp.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (= (bvcomp v1 (_ bv0 1)) ((_ extract 0 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2
new file mode 100644 (file)
index 0000000..e2941b3
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvconcat.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (concat (bvlshr (bvashr (bvudiv x0 x1) (bvurem x2 x3)) (bvudiv x4 x5)) (bvurem x6 x7)) ((_ extract 19 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2
new file mode 100644 (file)
index 0000000..aa901b9
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvconcat2.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= (concat x0 x0) (_ bv1 20)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2
new file mode 100644 (file)
index 0000000..d3cadf6
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvdiv.smt2
@@ -0,0 +1,33 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (bvshl (bvlshr (bvashr (bvudiv x0 x1) (bvurem x2 x3)) (bvudiv x4 x5)) (bvurem x6 x7)) ((_ extract 9 0) v4))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvdiv2.smt2 b/test/regress/regress0/unconstrained/bvdiv2.smt2
new file mode 100644 (file)
index 0000000..6314701
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvdiv2.smt2
@@ -0,0 +1,26 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (= (bvudiv x0 x0) (_ bv1 10))
+ )
+)
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2
new file mode 100644 (file)
index 0000000..56289e2
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvext.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (= ((_ extract 3 0) v1) ((_ extract 3 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2
new file mode 100644 (file)
index 0000000..9e1ecc1
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvite.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (ite (= x0 ((_ extract 9 0) v3)) ((_ extract 0 0) v4) (bvnot ((_
+     extract 0 0) v4))) ((_ extract 0 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2
new file mode 100644 (file)
index 0000000..fc56695
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvmul.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (bvmul x0 x1) ((_ extract 9 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2
new file mode 100644 (file)
index 0000000..89e4ff5
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvmul2.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= (bvmul x0 (_ bv2 10)) (_ bv1 10)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2
new file mode 100644 (file)
index 0000000..ea67a1b
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvmul3.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (bvmul x0 (_ bv15 10)) ((_ extract 9 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2
new file mode 100644 (file)
index 0000000..22fc7e7
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvnot.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (= (bvnot (bvneg v1)) ((_ extract 0 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2
new file mode 100644 (file)
index 0000000..702f9d7
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvsle x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2
new file mode 100644 (file)
index 0000000..b797fa4
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv513 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvsle x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2
new file mode 100644 (file)
index 0000000..4d89783
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvslt x0 (_ bv513 10)))
+(assert (not (bvsle x0 x1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2
new file mode 100644 (file)
index 0000000..8927a5f
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv510 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvsle x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2
new file mode 100644 (file)
index 0000000..1aceacb
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvsgt x1 (_ bv510 10)))
+(assert (not (bvsle x0 x1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2
new file mode 100644 (file)
index 0000000..f983756
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvslt x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2
new file mode 100644 (file)
index 0000000..e56500a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv510 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvslt x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2
new file mode 100644 (file)
index 0000000..a4af152
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvsgt x0 (_ bv510 10)))
+(assert (bvslt x0 x1))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2
new file mode 100644 (file)
index 0000000..d702b6d
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv513 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvslt x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2
new file mode 100644 (file)
index 0000000..f4b6a7a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvslt x1 (_ bv513 10)))
+(assert (bvslt x0 x1))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2
new file mode 100644 (file)
index 0000000..cbbb4cc
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvule x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2
new file mode 100644 (file)
index 0000000..0e6f591
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv1 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvule x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2
new file mode 100644 (file)
index 0000000..11e3a98
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvult x0 (_ bv1 10)))
+(assert (not (bvule x0 x1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2
new file mode 100644 (file)
index 0000000..b8d978b
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv1022 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvule x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2
new file mode 100644 (file)
index 0000000..cd927d0
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvugt x1 (_ bv1022 10)))
+(assert (not (bvule x0 x1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2
new file mode 100644 (file)
index 0000000..fb94994
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvult x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2
new file mode 100644 (file)
index 0000000..3fb4a0d
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv1022 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvult x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2
new file mode 100644 (file)
index 0000000..b11ab9d
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvugt x0 (_ bv1022 10)))
+(assert (bvult x0 x1))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2
new file mode 100644 (file)
index 0000000..8170ec2
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv1 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvult x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2
new file mode 100644 (file)
index 0000000..545bcbf
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvult x1 (_ bv1 10)))
+(assert (bvult x0 x1))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/files b/test/regress/regress0/unconstrained/files
new file mode 100644 (file)
index 0000000..8a0f488
--- /dev/null
+++ b/test/regress/regress0/unconstrained/files
@@ -0,0 +1,49 @@
+arith2.smt2
+arith3.smt2
+arith4.smt2
+arith5.smt2
+arith6.smt2
+arith7.smt2
+arith.smt2
+array1.smt2
+bvbool2.smt2
+bvbool3.smt2
+bvbool.smt2
+bvcmp.smt2
+bvconcat2.smt2
+bvconcat.smt2
+bvdiv2.smt2
+bvdiv.smt2
+bvext.smt2
+bvite.smt2
+bvmul2.smt2
+bvmul3.smt2
+bvmul.smt2
+bvnot.smt2
+bvsle2.smt2
+bvsle3.smt2
+bvsle4.smt2
+bvsle5.smt2
+bvsle.smt2
+bvslt2.smt2
+bvslt3.smt2
+bvslt4.smt2
+bvslt5.smt2
+bvslt.smt2
+bvule2.smt2
+bvule3.smt2
+bvule4.smt2
+bvule5.smt2
+bvule.smt2
+bvult2.smt2
+bvult3.smt2
+bvult4.smt2
+bvult5.smt2
+bvult.smt2
+geq.smt2
+gt.smt2
+leq.smt2
+lt.smt2
+uf1.smt2
+uf2.smt2
+xor.smt2

diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2
new file mode 100644 (file)
index 0000000..818bb55
--- /dev/null
+++ b/test/regress/regress0/unconstrained/geq.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (>= v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2
new file mode 100644 (file)
index 0000000..76b119e
--- /dev/null
+++ b/test/regress/regress0/unconstrained/gt.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (> v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2
new file mode 100644 (file)
index 0000000..6c03fc2
--- /dev/null
+++ b/test/regress/regress0/unconstrained/leq.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (<= v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2
new file mode 100644 (file)
index 0000000..637a640
--- /dev/null
+++ b/test/regress/regress0/unconstrained/lt.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (< v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2
new file mode 100644 (file)
index 0000000..0b2a95f
--- /dev/null
+++ b/test/regress/regress0/unconstrained/uf1.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (- v1)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/uf2.smt2 b/test/regress/regress0/unconstrained/uf2.smt2
new file mode 100644 (file)
index 0000000..0aa1617
--- /dev/null
+++ b/test/regress/regress0/unconstrained/uf2.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun a2 ((_ BitVec 1)) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= (a2 (_ bv0 1)) v3))
+(assert (= (a2 (_ bv1 1)) v3))
+(assert (not (= (a2 v1) v3)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2
new file mode 100644 (file)
index 0000000..4089bb5
--- /dev/null
+++ b/test/regress/regress0/unconstrained/xor.smt2
@@ -0,0 +1,33 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (xor (= (bvxor (bvxnor (bvadd (bvsub x0 ((_ extract 9 0) v3)) ((_ extract
+     9 0) v4)) ((_ extract 9 0) v5)) ((_ extract 19 10) v3)) ((_ extract 19 10)
+     v4)) (= v3 v4)) (= v4 v5))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)