diff options
67 files changed, 1436 insertions, 12 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 4d39ec60f..3532116bc 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -451,6 +451,15 @@ public: } /** + * 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 ade887b23..b9db8dace 100644 --- 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 1606d7bab..34ec624bc 100644 --- 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 dc1b47bde..3fa00baae 100644 --- 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 68485ca8a..14b3e3b42 100644 --- 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 10a37b712..f07815e2e 100644 --- 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 1341c048a..85d6fbdf8 100644 --- 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 f5e4f4630..60e48dba2 100644 --- 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 5be052947..197134b6a 100644 --- 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 caf7566b9..b7ad1d174 100644 --- 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 958f50276..711ff9b72 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -107,6 +107,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. */ Node apply(TNode t); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f72275cb2..4ed0bcb60 100644 --- 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 019818a5f..bc9f4c889 100644 --- 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 01b9648ff..e9ef7d959 100644 --- 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 e6135dacb..f48b45b49 100644 --- 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 index 000000000..241b78848 --- /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 index 000000000..dc2b27414 --- /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 index 000000000..f9e829e45 --- /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 index 000000000..83634a50a --- /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 index 000000000..8cb825a8d --- /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 index 000000000..de1e305bc --- /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 index 000000000..05653415f --- /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 index 000000000..6cc063ca4 --- /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 index 000000000..82f084e87 --- /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 index 000000000..0dded2a2f --- /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 index 000000000..949096224 --- /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 index 000000000..6f72246f0 --- /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 index 000000000..7c9362672 --- /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 index 000000000..ba7316324 --- /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 index 000000000..e2941b34a --- /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 index 000000000..aa901b9b0 --- /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 index 000000000..d3cadf6c8 --- /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 index 000000000..6314701b3 --- /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 index 000000000..56289e245 --- /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 index 000000000..9e1ecc193 --- /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 index 000000000..fc56695f5 --- /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 index 000000000..89e4ff569 --- /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 index 000000000..ea67a1b5a --- /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 index 000000000..22fc7e7d2 --- /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 index 000000000..702f9d7a0 --- /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 index 000000000..b797fa4e8 --- /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 index 000000000..4d897830c --- /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 index 000000000..8927a5f2e --- /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 index 000000000..1aceacbe3 --- /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 index 000000000..f98375653 --- /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 index 000000000..e56500ad2 --- /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 index 000000000..a4af152f1 --- /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 index 000000000..d702b6d1a --- /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 index 000000000..f4b6a7a63 --- /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 index 000000000..cbbb4cc6e --- /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 index 000000000..0e6f5916b --- /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 index 000000000..11e3a9877 --- /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 index 000000000..b8d978b71 --- /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 index 000000000..cd927d0c6 --- /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 index 000000000..fb94994b4 --- /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 index 000000000..3fb4a0d23 --- /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 index 000000000..b11ab9da3 --- /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 index 000000000..8170ec280 --- /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 index 000000000..545bcbf64 --- /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 index 000000000..8a0f48889 --- /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 index 000000000..818bb55b3 --- /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 index 000000000..76b119e42 --- /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 index 000000000..6c03fc254 --- /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 index 000000000..637a6407f --- /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 index 000000000..0b2a95f49 --- /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 index 000000000..0aa1617eb --- /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 index 000000000..4089bb5dc --- /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) |