summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arrays/theory_arrays.cpp107
-rw-r--r--src/theory/arrays/theory_arrays.h10
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h10
-rw-r--r--src/theory/model.cpp12
-rw-r--r--src/theory/model.h2
-rw-r--r--test/regress/regress0/aufbv/Makefile.am1
-rw-r--r--test/regress/regress0/aufbv/fuzz13.smt90
-rw-r--r--test/regress/regress0/auflia/Makefile.am5
-rw-r--r--test/regress/regress0/auflia/fuzz02.smt244
-rw-r--r--test/regress/regress0/auflia/fuzz03.smt15
-rw-r--r--test/regress/regress0/auflia/fuzz04.smt15
11 files changed, 452 insertions, 59 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 342e67654..3a109b51a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -423,7 +423,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert)
Assert(d_equalityEngine.getRepresentative(store) == store);
d_infoMap.addIndex(store, node[1]);
if (internalAssert) {
- d_readsInternal.push_back(node);
+ d_readsInternal.insert(node);
}
d_reads.push_back(node);
Assert((d_isPreRegistered.insert(node), true));
@@ -445,7 +445,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert)
NodeManager* nm = NodeManager::currentNM();
Node ni = nm->mkNode(kind::SELECT, node, i);
if (!d_equalityEngine.hasTerm(ni)) {
- preRegisterTermInternal(ni);
+ preRegisterTermInternal(ni, false);
}
// Apply RIntro1 Rule
@@ -649,81 +649,80 @@ void TheoryArrays::computeCareGraph()
/////////////////////////////////////////////////////////////////////////////
-void TheoryArrays::collectReads(TNode n, set<Node>& readSet, set<Node>& cache)
+void TheoryArrays::collectTerms(TNode n, set<Node>& termSet)
{
- if (cache.find(n) != cache.end()) {
+ if (termSet.find(n) != termSet.end()) {
return;
}
- if (n.getKind() == kind::SELECT) {
- readSet.insert(n);
- }
- for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
- collectReads(*child_it, readSet, cache);
+ termSet.insert(n);
+ if (n.getType().isBoolean() || !isLeaf(n)) {
+ for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
+ collectTerms(*child_it, termSet);
+ }
}
- cache.insert(n);
}
-void TheoryArrays::collectArrays(TNode n, set<Node>& arraySet, set<Node>& cache)
+void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
{
- if (cache.find(n) != cache.end()) {
- return;
- }
- if (n.getType().isArray()) {
- arraySet.insert(n);
- }
- for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
- collectArrays(*child_it, arraySet, cache);
- }
- cache.insert(n);
-}
+ set<Node> termSet;
+ set<Node> cache;
-
-void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
- m->assertEqualityEngine( &d_equalityEngine );
-
- std::map<Node, std::vector<Node> > selects;
-
- set<Node> readSet, arraySet;
- set<Node> readCache, arrayCache;
- // Collect all arrays and selects appearing in assertions
+ // Collect all terms appearing in assertions
context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
for (; assert_it != assert_it_end; ++assert_it) {
- collectReads(*assert_it, readSet, readCache);
- collectArrays(*assert_it, arraySet, arrayCache);
+ collectTerms(*assert_it, termSet);
}
- // Add arrays and selects that are shared terms
+ // Add terms that are shared terms
context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
- for (; shared_it != shared_it_end; ++ shared_it) {
- collectReads(*shared_it, readSet, readCache);
- collectArrays(*shared_it, arraySet, arrayCache);
+ for (; shared_it != shared_it_end; ++shared_it) {
+ collectTerms(*shared_it, termSet);
}
// Add selects that were generated internally
- unsigned size = d_readsInternal.size();
- for (unsigned i = 0; i < size; ++i) {
- readSet.insert(d_readsInternal[i]);
+ context::CDHashSet<TNode, TNodeHashFunction>::iterator internal_it = d_readsInternal.begin(), internal_it_end = d_readsInternal.end();
+ for (; internal_it != internal_it_end; ++internal_it) {
+ termSet.insert(*internal_it);
}
// Go through all equivalence classes and collect relevant arrays and reads
std::vector<Node> arrays;
+ std::map<Node, std::vector<Node> > selects;
+ bool computeRep, isArray;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
- bool computeRep;
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
+ isArray = eqc.getType().isArray();
computeRep = false;
eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
while( !eqc_i.isFinished() ){
Node n = *eqc_i;
// If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
- if (!computeRep && n.getKind() != kind::STORE && arraySet.find(n) != arraySet.end()) {
- arrays.push_back(eqc);
- computeRep = true;
+ if (isArray && termSet.find(n) != termSet.end()) {
+ if (n.getKind() == kind::STORE) {
+ // Make sure RIntro1 reads are included
+ termSet.insert(NodeManager::currentNM()->mkNode(kind::SELECT, n, n[1]));
+ }
+ else if (!computeRep) {
+ arrays.push_back(eqc);
+ computeRep = true;
+ }
}
- // If this term is a select, and it appears in an assertion or was generated internally,
+ ++eqc_i;
+ }
+ ++eqcs_i;
+ }
+
+ eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ Node n = *eqc_i;
+ // If this term is a select, and it appears in an assertion or was derived from one,
// record that the EC rep of its store parameter is being read from using this term
- if (n.getKind() == kind::SELECT && readSet.find(n) != readSet.end()) {
+ if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end()) {
selects[d_equalityEngine.getRepresentative(n[0])].push_back(n);
}
++eqc_i;
@@ -731,6 +730,8 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
++eqcs_i;
}
+ m->assertEqualityEngine(&d_equalityEngine, &termSet);
+
NodeManager* nm = NodeManager::currentNM();
Node rep;
map<Node, Node> defValues;
@@ -1259,6 +1260,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
Node i_eq_j = i.eqNode(j);
Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j);
d_permRef.push_back(reason);
+ d_readsInternal.insert(aj);
+ d_readsInternal.insert(bj);
if (!ajExists) {
preRegisterTermInternal(aj);
}
@@ -1301,6 +1304,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
// Make sure that any terms introduced by rewriting are appropriately stored in the equality database
Node aj2 = Rewriter::rewrite(aj);
if (aj != aj2) {
+ d_readsInternal.insert(aj);
+ d_readsInternal.insert(aj2);
if (!ajExists) {
preRegisterTermInternal(aj);
}
@@ -1311,6 +1316,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
}
Node bj2 = Rewriter::rewrite(bj);
if (bj != bj2) {
+ d_readsInternal.insert(bj);
+ d_readsInternal.insert(bj2);
if (!bjExists) {
preRegisterTermInternal(bj);
}
@@ -1327,6 +1334,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
Node eq1 = aj2.eqNode(bj2);
Node eq1_r = Rewriter::rewrite(eq1);
if (eq1_r == d_true) {
+ d_readsInternal.insert(aj2);
+ d_readsInternal.insert(bj2);
if (!d_equalityEngine.hasTerm(aj2)) {
preRegisterTermInternal(aj2);
}
@@ -1401,6 +1410,8 @@ void TheoryArrays::dischargeLemmas()
// Make sure that any terms introduced by rewriting are appropriately stored in the equality database
Node aj2 = Rewriter::rewrite(aj);
if (aj != aj2) {
+ d_readsInternal.insert(aj);
+ d_readsInternal.insert(aj2);
if (!ajExists) {
preRegisterTermInternal(aj);
}
@@ -1411,6 +1422,8 @@ void TheoryArrays::dischargeLemmas()
}
Node bj2 = Rewriter::rewrite(bj);
if (bj != bj2) {
+ d_readsInternal.insert(bj);
+ d_readsInternal.insert(bj2);
if (!bjExists) {
preRegisterTermInternal(bj);
}
@@ -1427,6 +1440,8 @@ void TheoryArrays::dischargeLemmas()
Node eq1 = aj2.eqNode(bj2);
Node eq1_r = Rewriter::rewrite(eq1);
if (eq1_r == d_true) {
+ d_readsInternal.insert(aj2);
+ d_readsInternal.insert(bj2);
if (!d_equalityEngine.hasTerm(aj2)) {
preRegisterTermInternal(aj2);
}
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index a47c8440e..9bf1201f3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -218,12 +218,12 @@ class TheoryArrays : public Theory {
/////////////////////////////////////////////////////////////////////////////
private:
- /** Helper functions for collectModelInfo */
- void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache);
- void collectArrays(TNode n, std::set<Node>& arraySet, std::set<Node>& cache);
+ /** Helper function for collectModelInfo */
+ void collectTerms(TNode n, std::set<Node>& termSet);
+
public:
- void collectModelInfo( TheoryModel* m, bool fullModel );
+ void collectModelInfo(TheoryModel* m, bool fullModel);
/////////////////////////////////////////////////////////////////////////////
// NOTIFICATIONS
@@ -337,7 +337,7 @@ class TheoryArrays : public Theory {
context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
context::CDO<bool> d_sharedTerms;
context::CDList<TNode> d_reads;
- context::CDList<TNode> d_readsInternal;
+ context::CDHashSet<TNode, TNodeHashFunction> d_readsInternal;
std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
// The decision requests we have for the core
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 62782f90e..da479616d 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -306,7 +306,15 @@ public:
NodeManager* nm = NodeManager::currentNM();
if (val) {
// store(store(a,i,v),i,w) = store(a,i,w)
- Node result = nm->mkNode(kind::STORE, store[0], index, value);
+ Node result;
+ if (value.getKind() == kind::SELECT &&
+ value[0] == store[0] &&
+ value[1] == index) {
+ result = store[0];
+ }
+ else {
+ result = nm->mkNode(kind::STORE, store[0], index, value);
+ }
Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl;
return RewriteResponse(REWRITE_DONE, result);
}
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index a01844f77..0e1d90a74 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -246,9 +246,10 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
}
/** assert equality engine */
-void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
+void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* termSet)
+{
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
- while( !eqcs_i.isFinished() ){
+ for (; !eqcs_i.isFinished(); ++eqcs_i) {
Node eqc = (*eqcs_i);
bool predicate = false;
bool predTrue = false;
@@ -259,7 +260,10 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
predFalse = ee->areEqual(eqc, d_false);
}
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
- while(!eqc_i.isFinished()) {
+ for (; !eqc_i.isFinished(); ++eqc_i) {
+ if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
+ continue;
+ }
if (predicate) {
if (predTrue) {
assertPredicate(*eqc_i, true);
@@ -275,9 +279,7 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
} else {
assertEquality(*eqc_i, eqc, true);
}
- ++eqc_i;
}
- ++eqcs_i;
}
}
diff --git a/src/theory/model.h b/src/theory/model.h
index 5b691d4d9..d17192281 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -92,7 +92,7 @@ public:
/** assert predicate holds in the model */
void assertPredicate( Node a, bool polarity );
/** assert all equalities/predicates in equality engine hold in the model */
- void assertEqualityEngine( const eq::EqualityEngine* ee );
+ void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
/** assert representative
* This function tells the model that n should be the representative of its equivalence class.
* It should be called during model generation, before final representatives are chosen. In the
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index 1a698b180..c67ce5b00 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -44,6 +44,7 @@ TESTS = \
fuzz10.smt \
fuzz11.smt \
fuzz12.smt \
+ fuzz13.smt \
fifo32bc06k08.delta01.smt \
rewrite_bug.smt \
array_rewrite_bug.smt
diff --git a/test/regress/regress0/aufbv/fuzz13.smt b/test/regress/regress0/aufbv/fuzz13.smt
new file mode 100644
index 000000000..d8c0b8480
--- /dev/null
+++ b/test/regress/regress0/aufbv/fuzz13.smt
@@ -0,0 +1,90 @@
+(benchmark fuzzsmt
+:logic QF_AUFBV
+:status sat
+:extrafuns ((v0 BitVec[9]))
+:extrafuns ((v1 BitVec[14]))
+:extrafuns ((a2 Array[2:5]))
+:extrafuns ((a3 Array[8:5]))
+:formula
+(let (?e4 bv712[10])
+(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1]))
+(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1))
+(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6)))
+(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1)))
+(let (?e9 (select ?e8 (extract[12:11] v1)))
+(let (?e10 (select a2 (extract[2:1] ?e4)))
+(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10))
+(let (?e12 (select ?e11 (extract[1:0] ?e10)))
+(let (?e13 (select a2 (extract[3:2] ?e9)))
+(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1]))
+(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13)))
+(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1]))
+(let (?e17 (extract[0:0] ?e5))
+(let (?e18 (zero_extend[0] ?e6))
+(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1))
+(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6))
+(flet ($e21 (bvugt v1 (zero_extend[9] ?e12)))
+(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14)))
+(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10)))
+(flet ($e24 (bvugt ?e19 v1))
+(flet ($e25 (bvult (sign_extend[4] ?e12) v0))
+(flet ($e26 (= (sign_extend[4] ?e15) v1))
+(flet ($e27 (= ?e19 (sign_extend[9] ?e12)))
+(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6))
+(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5)))
+(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9))
+(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12))
+(flet ($e32 (bvslt ?e10 ?e12))
+(flet ($e33 (distinct ?e6 ?e18))
+(flet ($e34 (bvsge (sign_extend[4] ?e12) v0))
+(flet ($e35 (bvsge ?e6 (zero_extend[5] v0)))
+(flet ($e36 (distinct v0 (sign_extend[4] ?e13)))
+(flet ($e37 (= ?e18 (sign_extend[5] v0)))
+(flet ($e38 (bvugt ?e16 ?e5))
+(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16)))
+(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19))
+(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5)))
+(flet ($e42 (bvslt (zero_extend[4] ?e12) v0))
+(flet ($e43 (bvugt ?e14 ?e17))
+(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13))
+(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12))
+(flet ($e46 (bvsge ?e19 ?e6))
+(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14)))
+(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4)))
+(flet ($e49 (and $e22 $e30))
+(flet ($e50 (or $e38 $e29))
+(flet ($e51 (xor $e41 $e34))
+(flet ($e52 (iff $e21 $e48))
+(flet ($e53 (iff $e46 $e23))
+(flet ($e54 (iff $e33 $e44))
+(flet ($e55 (and $e24 $e43))
+(flet ($e56 (implies $e32 $e31))
+(flet ($e57 (or $e56 $e47))
+(flet ($e58 (xor $e50 $e40))
+(flet ($e59 (or $e57 $e45))
+(flet ($e60 (iff $e42 $e59))
+(flet ($e61 (or $e35 $e36))
+(flet ($e62 (if_then_else $e51 $e60 $e25))
+(flet ($e63 (or $e55 $e54))
+(flet ($e64 (xor $e53 $e39))
+(flet ($e65 (and $e63 $e63))
+(flet ($e66 (or $e61 $e28))
+(flet ($e67 (and $e27 $e27))
+(flet ($e68 (or $e26 $e26))
+(flet ($e69 (or $e65 $e49))
+(flet ($e70 (xor $e58 $e62))
+(flet ($e71 (implies $e68 $e37))
+(flet ($e72 (if_then_else $e52 $e52 $e70))
+(flet ($e73 (implies $e66 $e67))
+(flet ($e74 (xor $e64 $e71))
+(flet ($e75 (and $e73 $e73))
+(flet ($e76 (implies $e72 $e69))
+(flet ($e77 (xor $e76 $e75))
+(flet ($e78 (iff $e77 $e74))
+(flet ($e79 (and $e78 (not (= v1 bv0[14]))))
+(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14])))))
+(flet ($e81 (and $e80 (not (= ?e6 bv0[14]))))
+(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14])))))
+$e82
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index 362209579..ed810eaeb 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -15,7 +15,10 @@ endif
TESTS = \
bug330.smt2 \
bug336.smt2 \
- fuzz01.delta01.smt
+ fuzz01.delta01.smt \
+ fuzz02.smt \
+ fuzz03.smt \
+ fuzz04.smt
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/auflia/fuzz02.smt b/test/regress/regress0/auflia/fuzz02.smt
new file mode 100644
index 000000000..7f34226e7
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz02.smt
@@ -0,0 +1,244 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:status sat
+:extrafuns ((f0 Int Int))
+:extrafuns ((f1 Array Array))
+:extrapreds ((p0 Int Int Int))
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v0 Int))
+:extrafuns ((v1 Int))
+:extrafuns ((v2 Array))
+:extrafuns ((v3 Array))
+:formula
+(let (?e4 1)
+(let (?e5 (+ v0 v0))
+(let (?e6 (f0 v0))
+(let (?e7 (ite (p0 ?e6 v1 ?e5) 1 0))
+(let (?e8 (* v0 ?e4))
+(let (?e9 (select v3 ?e6))
+(let (?e10 (select v3 ?e5))
+(let (?e11 (f1 v3))
+(let (?e12 (f1 ?e11))
+(let (?e13 (f1 ?e12))
+(let (?e14 (f1 v2))
+(flet ($e15 (p1 v3 v3 v3))
+(flet ($e16 (p1 ?e11 ?e11 ?e13))
+(flet ($e17 (p1 ?e14 ?e13 ?e12))
+(flet ($e18 (p1 v2 v3 ?e11))
+(flet ($e19 (p0 v1 ?e9 v0))
+(flet ($e20 (p0 ?e8 v1 ?e7))
+(flet ($e21 (> v0 ?e6))
+(flet ($e22 (< ?e5 ?e10))
+(let (?e23 (ite $e20 ?e12 ?e12))
+(let (?e24 (ite $e21 ?e23 v3))
+(let (?e25 (ite $e22 ?e13 ?e12))
+(let (?e26 (ite $e18 v2 ?e24))
+(let (?e27 (ite $e15 ?e11 ?e26))
+(let (?e28 (ite $e22 ?e14 ?e26))
+(let (?e29 (ite $e16 ?e13 ?e23))
+(let (?e30 (ite $e17 ?e11 ?e28))
+(let (?e31 (ite $e19 ?e13 ?e11))
+(let (?e32 (ite $e21 v0 ?e7))
+(let (?e33 (ite $e20 ?e8 v1))
+(let (?e34 (ite $e20 ?e32 ?e32))
+(let (?e35 (ite $e16 v1 ?e8))
+(let (?e36 (ite $e17 ?e6 ?e7))
+(let (?e37 (ite $e19 ?e32 ?e7))
+(let (?e38 (ite $e21 ?e9 ?e8))
+(let (?e39 (ite $e15 ?e10 ?e37))
+(let (?e40 (ite $e19 ?e7 ?e6))
+(let (?e41 (ite $e22 ?e5 ?e8))
+(let (?e42 (ite $e18 ?e32 ?e8))
+(let (?e43 (select ?e13 ?e35))
+(let (?e44 (select ?e26 ?e37))
+(let (?e45 (f1 ?e26))
+(let (?e46 (f1 ?e12))
+(let (?e47 (f1 ?e25))
+(let (?e48 (f1 ?e25))
+(let (?e49 (f1 ?e24))
+(let (?e50 (f1 ?e14))
+(let (?e51 (f1 ?e23))
+(let (?e52 (f1 ?e27))
+(let (?e53 (f1 ?e30))
+(let (?e54 (f1 ?e29))
+(let (?e55 (f1 ?e31))
+(let (?e56 (f1 v3))
+(let (?e57 (f1 ?e50))
+(let (?e58 (f1 ?e13))
+(let (?e59 (f1 ?e11))
+(let (?e60 (f1 ?e12))
+(let (?e61 (f1 ?e28))
+(let (?e62 (f1 ?e49))
+(let (?e63 (f1 v2))
+(let (?e64 (f0 ?e36))
+(let (?e65 (+ v0 ?e36))
+(let (?e66 (- v1 ?e35))
+(let (?e67 (f0 ?e65))
+(let (?e68 (f0 ?e32))
+(let (?e69 (f0 ?e6))
+(let (?e70 (- ?e35 ?e68))
+(let (?e71 (* ?e4 ?e40))
+(let (?e72 (~ ?e42))
+(let (?e73 (- ?e38 ?e37))
+(let (?e74 (~ ?e39))
+(let (?e75 (ite (p0 ?e64 ?e34 ?e70) 1 0))
+(let (?e76 (- ?e10 ?e5))
+(let (?e77 (* ?e41 ?e4))
+(let (?e78 (ite (p0 ?e73 ?e7 ?e34) 1 0))
+(let (?e79 (~ ?e10))
+(let (?e80 (- ?e42 ?e64))
+(let (?e81 (* ?e10 (~ ?e4)))
+(let (?e82 (+ ?e9 ?e69))
+(let (?e83 (- ?e34 ?e39))
+(let (?e84 (~ ?e33))
+(let (?e85 (+ ?e43 ?e33))
+(let (?e86 (- ?e37 ?e37))
+(let (?e87 (ite (p0 ?e5 ?e64 ?e83) 1 0))
+(let (?e88 (f0 ?e74))
+(let (?e89 (ite (p0 ?e88 ?e9 ?e73) 1 0))
+(let (?e90 (+ ?e88 ?e80))
+(let (?e91 (- ?e8 ?e8))
+(let (?e92 (~ ?e44))
+(flet ($e93 (p1 ?e52 ?e59 ?e30))
+(flet ($e94 (p1 ?e61 ?e29 ?e46))
+(flet ($e95 (p1 ?e51 ?e50 ?e63))
+(flet ($e96 (p1 ?e13 ?e63 ?e23))
+(flet ($e97 (p1 ?e57 ?e25 ?e57))
+(flet ($e98 (p1 v2 ?e58 ?e31))
+(flet ($e99 (p1 ?e14 ?e28 ?e14))
+(flet ($e100 (p1 ?e62 ?e57 ?e30))
+(flet ($e101 (p1 ?e53 ?e12 ?e62))
+(flet ($e102 (p1 ?e49 ?e12 ?e52))
+(flet ($e103 (p1 ?e46 ?e49 ?e14))
+(flet ($e104 (p1 ?e57 v2 ?e31))
+(flet ($e105 (p1 ?e24 ?e55 ?e14))
+(flet ($e106 (p1 ?e53 ?e59 ?e30))
+(flet ($e107 (p1 v3 ?e11 ?e30))
+(flet ($e108 (p1 ?e56 ?e59 ?e60))
+(flet ($e109 (p1 ?e62 ?e23 ?e55))
+(flet ($e110 (p1 ?e29 ?e59 ?e51))
+(flet ($e111 (p1 ?e30 ?e28 ?e59))
+(flet ($e112 (p1 v2 ?e54 ?e13))
+(flet ($e113 (p1 ?e14 ?e50 ?e48))
+(flet ($e114 (p1 ?e26 ?e60 ?e30))
+(flet ($e115 (p1 ?e27 ?e12 ?e47))
+(flet ($e116 (p1 ?e45 ?e53 ?e62))
+(flet ($e117 (<= ?e91 ?e85))
+(flet ($e118 (>= ?e40 ?e89))
+(flet ($e119 (distinct ?e76 ?e77))
+(flet ($e120 (>= ?e91 ?e5))
+(flet ($e121 (= ?e84 ?e68))
+(flet ($e122 (p0 ?e41 v1 ?e36))
+(flet ($e123 (= ?e77 ?e69))
+(flet ($e124 (> ?e38 ?e10))
+(flet ($e125 (p0 v1 ?e77 ?e5))
+(flet ($e126 (= ?e64 ?e41))
+(flet ($e127 (>= ?e81 ?e40))
+(flet ($e128 (< ?e67 ?e39))
+(flet ($e129 (distinct ?e78 ?e65))
+(flet ($e130 (<= ?e34 ?e33))
+(flet ($e131 (<= ?e72 ?e76))
+(flet ($e132 (> ?e87 ?e88))
+(flet ($e133 (>= ?e92 ?e8))
+(flet ($e134 (>= ?e86 ?e36))
+(flet ($e135 (> ?e32 ?e33))
+(flet ($e136 (distinct ?e90 ?e6))
+(flet ($e137 (< ?e88 ?e35))
+(flet ($e138 (p0 ?e9 ?e38 ?e78))
+(flet ($e139 (> ?e80 ?e32))
+(flet ($e140 (p0 ?e79 ?e91 ?e88))
+(flet ($e141 (p0 ?e75 ?e10 ?e74))
+(flet ($e142 (>= ?e34 ?e39))
+(flet ($e143 (p0 ?e66 ?e67 ?e66))
+(flet ($e144 (= ?e90 ?e39))
+(flet ($e145 (< ?e37 ?e79))
+(flet ($e146 (distinct ?e44 ?e78))
+(flet ($e147 (< ?e83 v0))
+(flet ($e148 (>= ?e7 ?e69))
+(flet ($e149 (>= ?e73 ?e10))
+(flet ($e150 (p0 ?e71 ?e90 ?e65))
+(flet ($e151 (p0 ?e36 ?e33 ?e33))
+(flet ($e152 (> ?e82 ?e80))
+(flet ($e153 (distinct ?e79 ?e10))
+(flet ($e154 (p0 ?e42 ?e64 v0))
+(flet ($e155 (< ?e70 ?e86))
+(flet ($e156 (<= ?e43 ?e7))
+(flet ($e157 (or $e16 $e139))
+(flet ($e158 (if_then_else $e103 $e93 $e141))
+(flet ($e159 (not $e132))
+(flet ($e160 (or $e111 $e100))
+(flet ($e161 (iff $e160 $e134))
+(flet ($e162 (and $e19 $e133))
+(flet ($e163 (and $e146 $e128))
+(flet ($e164 (and $e157 $e156))
+(flet ($e165 (xor $e140 $e155))
+(flet ($e166 (implies $e113 $e153))
+(flet ($e167 (iff $e164 $e102))
+(flet ($e168 (implies $e121 $e116))
+(flet ($e169 (if_then_else $e142 $e119 $e104))
+(flet ($e170 (implies $e129 $e99))
+(flet ($e171 (or $e135 $e161))
+(flet ($e172 (or $e126 $e15))
+(flet ($e173 (implies $e158 $e137))
+(flet ($e174 (iff $e166 $e117))
+(flet ($e175 (iff $e105 $e174))
+(flet ($e176 (not $e125))
+(flet ($e177 (iff $e120 $e171))
+(flet ($e178 (xor $e168 $e149))
+(flet ($e179 (and $e96 $e96))
+(flet ($e180 (and $e130 $e143))
+(flet ($e181 (and $e108 $e20))
+(flet ($e182 (if_then_else $e173 $e159 $e167))
+(flet ($e183 (xor $e118 $e107))
+(flet ($e184 (implies $e98 $e169))
+(flet ($e185 (and $e177 $e136))
+(flet ($e186 (not $e185))
+(flet ($e187 (and $e170 $e138))
+(flet ($e188 (iff $e109 $e147))
+(flet ($e189 (or $e188 $e145))
+(flet ($e190 (implies $e152 $e94))
+(flet ($e191 (if_then_else $e97 $e181 $e163))
+(flet ($e192 (iff $e115 $e190))
+(flet ($e193 (if_then_else $e183 $e172 $e17))
+(flet ($e194 (not $e127))
+(flet ($e195 (iff $e179 $e101))
+(flet ($e196 (iff $e186 $e154))
+(flet ($e197 (if_then_else $e178 $e176 $e150))
+(flet ($e198 (xor $e122 $e124))
+(flet ($e199 (not $e182))
+(flet ($e200 (and $e112 $e197))
+(flet ($e201 (iff $e151 $e184))
+(flet ($e202 (or $e106 $e192))
+(flet ($e203 (iff $e162 $e95))
+(flet ($e204 (and $e199 $e199))
+(flet ($e205 (if_then_else $e131 $e187 $e131))
+(flet ($e206 (xor $e144 $e201))
+(flet ($e207 (and $e18 $e202))
+(flet ($e208 (and $e193 $e22))
+(flet ($e209 (or $e123 $e203))
+(flet ($e210 (not $e196))
+(flet ($e211 (and $e209 $e200))
+(flet ($e212 (xor $e208 $e114))
+(flet ($e213 (xor $e212 $e175))
+(flet ($e214 (and $e148 $e206))
+(flet ($e215 (or $e198 $e210))
+(flet ($e216 (or $e213 $e215))
+(flet ($e217 (xor $e189 $e194))
+(flet ($e218 (and $e214 $e204))
+(flet ($e219 (and $e211 $e21))
+(flet ($e220 (and $e165 $e191))
+(flet ($e221 (xor $e180 $e180))
+(flet ($e222 (and $e218 $e205))
+(flet ($e223 (iff $e195 $e219))
+(flet ($e224 (not $e221))
+(flet ($e225 (iff $e222 $e220))
+(flet ($e226 (implies $e225 $e223))
+(flet ($e227 (not $e207))
+(flet ($e228 (if_then_else $e226 $e226 $e216))
+(flet ($e229 (iff $e217 $e110))
+(flet ($e230 (not $e229))
+(flet ($e231 (if_then_else $e224 $e230 $e227))
+(flet ($e232 (or $e231 $e228))
+$e232
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
diff --git a/test/regress/regress0/auflia/fuzz03.smt b/test/regress/regress0/auflia/fuzz03.smt
new file mode 100644
index 000000000..151250a1f
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz03.smt
@@ -0,0 +1,15 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrapreds ((p1 Array Array Array))
+:extrafuns ((v1 Array))
+:extrafuns ((f1 Array Array Array Array))
+:status sat
+:formula
+(let (?n1 0)
+(let (?n2 (store v1 ?n1 ?n1))
+(let (?n3 (f1 v1 v1 ?n2))
+(let (?n4 (f1 v1 ?n2 v1))
+(let (?n5 (f1 v1 ?n4 ?n2))
+(flet ($n6 (p1 ?n3 ?n5 v1))
+$n6
+)))))))
diff --git a/test/regress/regress0/auflia/fuzz04.smt b/test/regress/regress0/auflia/fuzz04.smt
new file mode 100644
index 000000000..7523aae28
--- /dev/null
+++ b/test/regress/regress0/auflia/fuzz04.smt
@@ -0,0 +1,15 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrapreds ((p1 Array Array))
+:extrafuns ((f1 Array Array Array Array))
+:extrafuns ((v3 Array))
+:status sat
+:formula
+(let (?n1 (f1 v3 v3 v3))
+(let (?n2 0)
+(let (?n3 (store v3 ?n2 ?n2))
+(let (?n4 (f1 v3 v3 ?n3))
+(let (?n5 (f1 v3 ?n4 v3))
+(flet ($n6 (p1 ?n1 ?n5))
+$n6
+)))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback