Fix stale reference in MiniSat when generating UC (#2113)

In MiniSat's analyze(), we were taking a reference of a clause that
could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can
lead to allocation of clauses which in turn can lead to clauses being
reallocated, making the reference stale. The commit encloses the
reference in a code block that makes the lifetime of the reference more
obvious and removes uses of the potentially stale reference.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 3c802339563278b344e66a77ec49add056d3cb91..8f5b37e74def7286969dc974adf571ff29e55ccd 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -698,34 +698,49 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     PROOF( ProofManager::getSatProof()->startResChain(confl); )
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
-        Clause& c = ca[confl];
-        max_resolution_level = std::max(max_resolution_level, c.level());
-
-        if (c.removable())
-            claBumpActivity(c);
-
-        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
-            Lit q = c[j];
-
-            if (!seen[var(q)] && level(var(q)) > 0) {
-                varBumpActivity(var(q));
-                seen[var(q)] = 1;
-                if (level(var(q)) >= decisionLevel())
-                    pathC++;
-                else
-                    out_learnt.push(q);
-            } else {
-              // We could be resolving a literal propagated by a clause/theory using
-              // information from a higher level
-              if (!seen[var(q)] && level(var(q)) == 0) {
-                max_resolution_level = std::max(max_resolution_level, user_level(var(q)));
-              }
 
-              // FIXME: can we do it lazily if we actually need the proof?
-              if (level(var(q)) == 0) {
-                PROOF( ProofManager::getSatProof()->resolveOutUnit(q); )
-              }
+        {
+          // ! IMPORTANT !
+          // It is not safe to use c after this block of code because
+          // resolveOutUnit() below may lead to clauses being allocated, which
+          // in turn may lead to reallocations that invalidate c.
+          Clause& c = ca[confl];
+          max_resolution_level = std::max(max_resolution_level, c.level());
+
+          if (c.removable()) claBumpActivity(c);
+        }
+
+        for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size();
+             j < size;
+             j++)
+        {
+          Lit q = ca[confl][j];
+
+          if (!seen[var(q)] && level(var(q)) > 0)
+          {
+            varBumpActivity(var(q));
+            seen[var(q)] = 1;
+            if (level(var(q)) >= decisionLevel())
+              pathC++;
+            else
+              out_learnt.push(q);
+          }
+          else
+          {
+            // We could be resolving a literal propagated by a clause/theory
+            // using information from a higher level
+            if (!seen[var(q)] && level(var(q)) == 0)
+            {
+              max_resolution_level =
+                  std::max(max_resolution_level, user_level(var(q)));
+            }
+
+            // FIXME: can we do it lazily if we actually need the proof?
+            if (level(var(q)) == 0)
+            {
+              PROOF(ProofManager::getSatProof()->resolveOutUnit(q);)
             }
+          }
         }
 
         // Select next clause to look at:

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 939b52128cec222d5ea817770c3ff8c33d7c27b0..83f1c07143e36c9ce5be84ad570388da6c9dac67 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1600,6 +1600,7 @@ REG2_TESTS = \
        regress2/ooo.rf6.smt2 \
        regress2/ooo.tag10.smt2 \
        regress2/piVC_5581bd.smt2 \
+       regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 \
        regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \
        regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \
        regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \

diff --git a/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 b/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
new file mode 100644 (file)
index 0000000..cdaefbf
--- /dev/null
+++ b/test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
@@ -0,0 +1,1182 @@
+; COMMAND-LINE: --check-unsat-cores --incremental
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun _substvar_577_ () Int)
+(declare-fun _substvar_578_ () Int)
+(declare-fun _substvar_579_ () Int)
+(declare-fun _substvar_580_ () Int)
+(declare-fun _substvar_581_ () Int)
+(declare-fun _substvar_582_ () Int)
+(declare-fun _substvar_583_ () Int)
+(declare-fun _substvar_584_ () Int)
+(declare-fun _substvar_585_ () Int)
+(declare-fun _substvar_856_ () Int)
+(declare-fun _substvar_857_ () Int)
+(declare-fun _substvar_874_ () Int)
+(declare-fun _substvar_875_ () Int)
+(declare-fun _substvar_991_ () Int)
+(declare-fun _substvar_1089_ () Int)
+(declare-fun _substvar_4540_ () Bool)
+(declare-fun _substvar_4541_ () Bool)
+(declare-fun _substvar_4542_ () Bool)
+(declare-fun _substvar_4543_ () Bool)
+(declare-fun _substvar_4544_ () Bool)
+(declare-fun _substvar_4545_ () Bool)
+(declare-fun _substvar_4546_ () Bool)
+(declare-fun _substvar_4547_ () Bool)
+(declare-fun _substvar_4548_ () Bool)
+(declare-fun _substvar_4549_ () Bool)
+(declare-fun _substvar_4550_ () Bool)
+(declare-fun _substvar_5910_ () Bool)
+(declare-fun _substvar_5911_ () Bool)
+(declare-fun _substvar_5918_ () Bool)
+(declare-fun _substvar_5919_ () Bool)
+(declare-fun _substvar_5934_ () Bool)
+(declare-fun _substvar_5935_ () Bool)
+(declare-fun _substvar_5990_ () Bool)
+(declare-fun _substvar_5991_ () Bool)
+(declare-fun _substvar_6008_ () Bool)
+(declare-fun _substvar_6009_ () Bool)
+(declare-fun _substvar_6010_ () Bool)
+(declare-fun _substvar_6011_ () Bool)
+(declare-fun _substvar_6102_ () Bool)
+(declare-fun _substvar_6103_ () Bool)
+(declare-fun _substvar_6148_ () Bool)
+(declare-fun _substvar_6149_ () Bool)
+(declare-fun _substvar_6194_ () Bool)
+(declare-fun _substvar_6195_ () Bool)
+(declare-fun _substvar_6240_ () Bool)
+(declare-fun _substvar_6241_ () Bool)
+(declare-fun _substvar_6286_ () Bool)
+(declare-fun _substvar_6287_ () Bool)
+(declare-fun _substvar_6661_ () Bool)
+(declare-fun _substvar_6685_ () Bool)
+(declare-fun _substvar_6692_ () Bool)
+(declare-fun _substvar_6712_ () Bool)
+(declare-fun _substvar_6714_ () Bool)
+(declare-fun _substvar_6728_ () Bool)
+(declare-fun _substvar_6730_ () Bool)
+(declare-fun _substvar_6732_ () Bool)
+(declare-fun _substvar_6734_ () Bool)
+(declare-fun _substvar_6736_ () Bool)
+(declare-fun _substvar_6738_ () Bool)
+(declare-fun _substvar_6740_ () Bool)
+(declare-fun _substvar_6742_ () Bool)
+(declare-fun _substvar_6744_ () Bool)
+(declare-fun _substvar_6746_ () Bool)
+(declare-fun _substvar_6748_ () Bool)
+(declare-fun _substvar_6750_ () Bool)
+(declare-fun _substvar_6752_ () Bool)
+(declare-fun _substvar_6754_ () Bool)
+(declare-fun _substvar_6756_ () Bool)
+(declare-fun _substvar_6758_ () Bool)
+(declare-fun _substvar_6760_ () Bool)
+(declare-fun _substvar_6762_ () Bool)
+(declare-fun _substvar_6764_ () Bool)
+(declare-fun _substvar_6766_ () Bool)
+(declare-fun _substvar_6768_ () Bool)
+(declare-fun _substvar_6770_ () Bool)
+(declare-fun _substvar_6773_ () Bool)
+(declare-fun _substvar_6775_ () Bool)
+(declare-fun _substvar_6777_ () Bool)
+(declare-fun _substvar_6779_ () Bool)
+(declare-fun _substvar_6781_ () Bool)
+(declare-fun _substvar_6783_ () Bool)
+(declare-fun _substvar_6785_ () Bool)
+(declare-fun _substvar_6787_ () Bool)
+(declare-fun _substvar_6789_ () Bool)
+(declare-fun _substvar_6791_ () Bool)
+(declare-fun _substvar_6793_ () Bool)
+(declare-fun _substvar_6796_ () Bool)
+(declare-fun _substvar_6797_ () Bool)
+(declare-fun _substvar_6800_ () Bool)
+(declare-fun _substvar_6802_ () Bool)
+(declare-fun _substvar_6804_ () Bool)
+(declare-fun _substvar_6806_ () Bool)
+(declare-fun _substvar_6808_ () Bool)
+(declare-fun _substvar_6810_ () Bool)
+(declare-fun _substvar_6812_ () Bool)
+(declare-fun _substvar_6814_ () Bool)
+(declare-fun _substvar_6816_ () Bool)
+(declare-fun _substvar_6820_ () Bool)
+(declare-fun _substvar_6823_ () Bool)
+(declare-fun _substvar_6825_ () Bool)
+(declare-fun _substvar_6827_ () Bool)
+(declare-fun _substvar_6829_ () Bool)
+(declare-fun _substvar_6831_ () Bool)
+(declare-fun _substvar_6833_ () Bool)
+(declare-fun _substvar_6835_ () Bool)
+(declare-fun _substvar_6837_ () Bool)
+(declare-fun _substvar_6840_ () Bool)
+(declare-fun _substvar_6841_ () Bool)
+(declare-fun _substvar_6843_ () Bool)
+(declare-fun _substvar_6845_ () Bool)
+(declare-fun _substvar_6848_ () Bool)
+(declare-fun _substvar_6850_ () Bool)
+(declare-fun _substvar_6852_ () Bool)
+(declare-fun _substvar_6854_ () Bool)
+(declare-fun _substvar_6856_ () Bool)
+(declare-fun _substvar_6858_ () Bool)
+(declare-fun _substvar_6860_ () Bool)
+(declare-fun _substvar_6864_ () Bool)
+(declare-fun _substvar_6866_ () Bool)
+(declare-fun _substvar_6868_ () Bool)
+(declare-fun _substvar_6871_ () Bool)
+(declare-fun _substvar_6873_ () Bool)
+(declare-fun _substvar_6875_ () Bool)
+(declare-fun _substvar_6877_ () Bool)
+(declare-fun _substvar_6879_ () Bool)
+(declare-fun _substvar_6881_ () Bool)
+(declare-fun _substvar_6884_ () Bool)
+(declare-fun _substvar_6885_ () Bool)
+(declare-fun _substvar_6887_ () Bool)
+(declare-fun _substvar_6889_ () Bool)
+(declare-fun _substvar_6891_ () Bool)
+(declare-fun _substvar_6893_ () Bool)
+(declare-fun _substvar_6896_ () Bool)
+(declare-fun _substvar_6898_ () Bool)
+(declare-fun _substvar_6900_ () Bool)
+(declare-fun _substvar_6902_ () Bool)
+(declare-fun _substvar_6904_ () Bool)
+(declare-fun _substvar_6908_ () Bool)
+(declare-fun _substvar_6910_ () Bool)
+(declare-fun _substvar_6912_ () Bool)
+(declare-fun _substvar_6914_ () Bool)
+(declare-fun _substvar_6916_ () Bool)
+(declare-fun _substvar_6919_ () Bool)
+(declare-fun _substvar_6921_ () Bool)
+(declare-fun _substvar_6923_ () Bool)
+(declare-fun _substvar_6925_ () Bool)
+(declare-fun _substvar_6928_ () Bool)
+(declare-fun _substvar_6929_ () Bool)
+(declare-fun _substvar_6931_ () Bool)
+(declare-fun _substvar_6933_ () Bool)
+(declare-fun _substvar_6935_ () Bool)
+(declare-fun _substvar_6937_ () Bool)
+(declare-fun _substvar_6939_ () Bool)
+(declare-fun _substvar_6941_ () Bool)
+(declare-fun _substvar_6944_ () Bool)
+(declare-fun _substvar_6946_ () Bool)
+(declare-fun _substvar_6948_ () Bool)
+(declare-fun _substvar_6952_ () Bool)
+(declare-fun _substvar_6954_ () Bool)
+(declare-fun _substvar_6956_ () Bool)
+(declare-fun _substvar_6958_ () Bool)
+(declare-fun _substvar_6960_ () Bool)
+(declare-fun _substvar_6962_ () Bool)
+(declare-fun _substvar_6964_ () Bool)
+(declare-fun _substvar_6967_ () Bool)
+(declare-fun _substvar_6969_ () Bool)
+(declare-fun _substvar_6972_ () Bool)
+(declare-fun _substvar_6973_ () Bool)
+(declare-fun _substvar_6975_ () Bool)
+(declare-fun _substvar_6977_ () Bool)
+(declare-fun _substvar_6979_ () Bool)
+(declare-fun _substvar_6981_ () Bool)
+(declare-fun _substvar_6983_ () Bool)
+(declare-fun _substvar_6985_ () Bool)
+(declare-fun _substvar_6987_ () Bool)
+(declare-fun _substvar_6989_ () Bool)
+(declare-fun _substvar_6992_ () Bool)
+(declare-fun _substvar_6996_ () Bool)
+(declare-fun _substvar_6998_ () Bool)
+(declare-fun _substvar_7000_ () Bool)
+(declare-fun _substvar_7002_ () Bool)
+(declare-fun _substvar_7004_ () Bool)
+(declare-fun _substvar_7006_ () Bool)
+(declare-fun _substvar_7008_ () Bool)
+(declare-fun _substvar_7010_ () Bool)
+(declare-fun _substvar_7012_ () Bool)
+(declare-fun _substvar_7031_ () Bool)
+(declare-fun _substvar_7047_ () Bool)
+(declare-fun _substvar_7071_ () Bool)
+(declare-fun _substvar_7086_ () Bool)
+(declare-fun _substvar_7096_ () Bool)
+(declare-fun _substvar_7098_ () Bool)
+(declare-fun _substvar_7119_ () Bool)
+(declare-fun _substvar_7121_ () Bool)
+(declare-fun _substvar_7128_ () Bool)
+(declare-fun _substvar_7142_ () Bool)
+(declare-fun _substvar_7144_ () Bool)
+(declare-fun _substvar_7148_ () Bool)
+(declare-fun _substvar_7150_ () Bool)
+(declare-fun _substvar_7152_ () Bool)
+(declare-fun _substvar_7171_ () Bool)
+(declare-fun _substvar_7173_ () Bool)
+(declare-fun _substvar_7175_ () Bool)
+(declare-fun _substvar_7177_ () Bool)
+(declare-fun _substvar_7194_ () Bool)
+(declare-fun _substvar_7196_ () Bool)
+(declare-fun _substvar_7198_ () Bool)
+(declare-fun _substvar_7200_ () Bool)
+(declare-fun _substvar_7217_ () Bool)
+(declare-fun _substvar_7219_ () Bool)
+(declare-fun _substvar_7221_ () Bool)
+(declare-fun _substvar_7223_ () Bool)
+(declare-fun _substvar_7240_ () Bool)
+(declare-fun _substvar_7242_ () Bool)
+(declare-fun _substvar_7244_ () Bool)
+(declare-fun _substvar_7246_ () Bool)
+(declare-fun _substvar_7263_ () Bool)
+(declare-fun _substvar_7265_ () Bool)
+(declare-fun _substvar_7267_ () Bool)
+(declare-fun _substvar_7269_ () Bool)
+(declare-fun _substvar_7286_ () Bool)
+(declare-fun _substvar_7288_ () Bool)
+(declare-fun _substvar_7290_ () Bool)
+(declare-fun _substvar_7292_ () Bool)
+(declare-fun _substvar_7302_ () Bool)
+(declare-fun _substvar_7309_ () Bool)
+(declare-fun _substvar_7311_ () Bool)
+(declare-fun _substvar_7313_ () Bool)
+(declare-fun _substvar_7315_ () Bool)
+(declare-fun _substvar_7317_ () Bool)
+(declare-fun _substvar_7325_ () Bool)
+(declare-fun _substvar_7327_ () Bool)
+(declare-fun _substvar_7332_ () Bool)
+(declare-fun _substvar_7336_ () Bool)
+(declare-fun _substvar_7341_ () Bool)
+(declare-fun _substvar_7344_ () Bool)
+(declare-fun _substvar_10006_ () Bool)
+(declare-fun _substvar_10007_ () Bool)
+(declare-fun _substvar_10008_ () Bool)
+(declare-fun _substvar_10009_ () Bool)
+(declare-fun _substvar_10010_ () Bool)
+(declare-fun _substvar_10011_ () Bool)
+(declare-fun _substvar_10012_ () Bool)
+(declare-fun _substvar_10013_ () Bool)
+(declare-fun _substvar_10014_ () Bool)
+(declare-fun _substvar_10015_ () Bool)
+(declare-fun _substvar_10016_ () Bool)
+(declare-fun _substvar_10017_ () Bool)
+(declare-fun _substvar_10018_ () Bool)
+(declare-fun _substvar_10019_ () Bool)
+(declare-fun _substvar_10020_ () Bool)
+(declare-fun _substvar_10021_ () Bool)
+(declare-fun _substvar_10022_ () Bool)
+(declare-fun _substvar_10023_ () Bool)
+(declare-fun _substvar_10024_ () Bool)
+(declare-fun _substvar_10025_ () Bool)
+(declare-fun _substvar_10026_ () Bool)
+(declare-fun _substvar_10027_ () Bool)
+(declare-fun _substvar_10028_ () Bool)
+(declare-fun _substvar_10029_ () Bool)
+(declare-fun _substvar_10030_ () Bool)
+(declare-fun _substvar_10031_ () Bool)
+(declare-fun _substvar_10032_ () Bool)
+(declare-fun _substvar_10033_ () Bool)
+(declare-fun _substvar_10034_ () Bool)
+(declare-fun _substvar_10035_ () Bool)
+(declare-fun _substvar_10036_ () Bool)
+(declare-fun _substvar_10037_ () Bool)
+(declare-fun _substvar_10038_ () Bool)
+(declare-fun _substvar_10039_ () Bool)
+(declare-fun _substvar_10040_ () Bool)
+(declare-fun _substvar_10041_ () Bool)
+(declare-fun _substvar_10042_ () Bool)
+(declare-fun _substvar_10043_ () Bool)
+(declare-fun _substvar_10044_ () Bool)
+(declare-fun _substvar_10045_ () Bool)
+(declare-fun _substvar_10046_ () Bool)
+(declare-fun _substvar_11989_ () Bool)
+(declare-fun _substvar_11990_ () Bool)
+(declare-fun _substvar_11991_ () Bool)
+(declare-fun _substvar_11992_ () Bool)
+(declare-fun _substvar_11993_ () Bool)
+(declare-fun _substvar_12034_ () Bool)
+(declare-fun _substvar_12035_ () Bool)
+(declare-fun _substvar_12036_ () Bool)
+(declare-fun _substvar_12037_ () Bool)
+(declare-fun _substvar_12038_ () Bool)
+(declare-fun _substvar_12064_ () Bool)
+(declare-fun _substvar_12065_ () Bool)
+(declare-fun _substvar_12066_ () Bool)
+(declare-fun _substvar_12067_ () Bool)
+(declare-fun _substvar_12068_ () Bool)
+(declare-fun _substvar_12124_ () Bool)
+(declare-fun _substvar_12125_ () Bool)
+(declare-fun _substvar_12126_ () Bool)
+(declare-fun _substvar_12127_ () Bool)
+(declare-fun _substvar_12128_ () Bool)
+(declare-fun _substvar_12129_ () Bool)
+(declare-fun _substvar_12130_ () Bool)
+(declare-fun _substvar_12131_ () Bool)
+(declare-fun _substvar_12132_ () Bool)
+(declare-fun _substvar_12133_ () Bool)
+(declare-fun _substvar_12169_ () Bool)
+(declare-fun _substvar_12170_ () Bool)
+(declare-fun _substvar_12171_ () Bool)
+(declare-fun _substvar_12172_ () Bool)
+(declare-fun _substvar_12173_ () Bool)
+(declare-fun _substvar_12184_ () Bool)
+(declare-fun _substvar_12185_ () Bool)
+(declare-fun _substvar_12186_ () Bool)
+(declare-fun _substvar_12187_ () Bool)
+(declare-fun _substvar_12188_ () Bool)
+(declare-fun _substvar_12199_ () Bool)
+(declare-fun _substvar_12200_ () Bool)
+(declare-fun _substvar_12201_ () Bool)
+(declare-fun _substvar_12202_ () Bool)
+(declare-fun _substvar_12203_ () Bool)
+(declare-fun _substvar_12209_ () Bool)
+(declare-fun _substvar_12210_ () Bool)
+(declare-fun _substvar_12211_ () Bool)
+(declare-fun _substvar_12212_ () Bool)
+(declare-fun _substvar_12213_ () Bool)
+(declare-fun _substvar_12284_ () Bool)
+(declare-fun _substvar_12285_ () Bool)
+(declare-fun _substvar_12286_ () Bool)
+(declare-fun _substvar_12287_ () Bool)
+(declare-fun _substvar_12288_ () Bool)
+(declare-fun _substvar_12289_ () Bool)
+(declare-fun _substvar_12290_ () Bool)
+(declare-fun _substvar_12291_ () Bool)
+(declare-fun _substvar_12292_ () Bool)
+(declare-fun _substvar_12293_ () Bool)
+(declare-fun _substvar_12319_ () Bool)
+(declare-fun _substvar_12320_ () Bool)
+(declare-fun _substvar_12321_ () Bool)
+(declare-fun _substvar_12322_ () Bool)
+(declare-fun _substvar_12323_ () Bool)
+(declare-fun _substvar_12434_ () Bool)
+(declare-fun _substvar_12435_ () Bool)
+(declare-fun _substvar_12436_ () Bool)
+(declare-fun _substvar_12437_ () Bool)
+(declare-fun _substvar_12438_ () Bool)
+(declare-fun _substvar_12439_ () Bool)
+(declare-fun _substvar_12440_ () Bool)
+(declare-fun _substvar_12441_ () Bool)
+(declare-fun _substvar_12442_ () Bool)
+(declare-fun _substvar_12443_ () Bool)
+(declare-fun _substvar_12534_ () Bool)
+(declare-fun _substvar_12535_ () Bool)
+(declare-fun _substvar_12536_ () Bool)
+(declare-fun _substvar_12537_ () Bool)
+(declare-fun _substvar_12538_ () Bool)
+(declare-fun _substvar_12543_ () Bool)
+(declare-fun _substvar_12544_ () Bool)
+(declare-fun _substvar_12573_ () Bool)
+(declare-fun _substvar_12574_ () Bool)
+(declare-fun _substvar_12583_ () Bool)
+(declare-fun _substvar_12584_ () Bool)
+(declare-fun _substvar_12591_ () Bool)
+(declare-fun _substvar_12592_ () Bool)
+(declare-fun _substvar_12605_ () Bool)
+(declare-fun _substvar_12606_ () Bool)
+(declare-fun _substvar_12611_ () Bool)
+(declare-fun _substvar_12612_ () Bool)
+(declare-fun _substvar_12619_ () Bool)
+(declare-fun _substvar_12620_ () Bool)
+(declare-fun _substvar_12627_ () Bool)
+(declare-fun _substvar_12628_ () Bool)
+(declare-fun _substvar_12631_ () Bool)
+(declare-fun _substvar_12632_ () Bool)
+(declare-fun _substvar_12633_ () Bool)
+(declare-fun _substvar_12634_ () Bool)
+(declare-fun _substvar_12643_ () Bool)
+(declare-fun _substvar_12644_ () Bool)
+(declare-fun _substvar_12647_ () Bool)
+(declare-fun _substvar_12648_ () Bool)
+(declare-fun _substvar_12649_ () Bool)
+(declare-fun _substvar_12650_ () Bool)
+(declare-fun _substvar_12659_ () Bool)
+(declare-fun _substvar_12660_ () Bool)
+(declare-fun _substvar_12663_ () Bool)
+(declare-fun _substvar_12664_ () Bool)
+(declare-fun _substvar_12669_ () Bool)
+(declare-fun _substvar_12670_ () Bool)
+(declare-fun _substvar_12671_ () Bool)
+(declare-fun _substvar_12672_ () Bool)
+(declare-fun _substvar_12673_ () Bool)
+(declare-fun _substvar_12674_ () Bool)
+(declare-fun _substvar_12681_ () Bool)
+(declare-fun _substvar_12682_ () Bool)
+(declare-fun _substvar_12687_ () Bool)
+(declare-fun _substvar_12688_ () Bool)
+(declare-fun _substvar_12691_ () Bool)
+(declare-fun _substvar_12692_ () Bool)
+(declare-fun _substvar_12695_ () Bool)
+(declare-fun _substvar_12696_ () Bool)
+(declare-fun _substvar_12699_ () Bool)
+(declare-fun _substvar_12700_ () Bool)
+(declare-fun _substvar_12721_ () Bool)
+(declare-fun _substvar_12722_ () Bool)
+(declare-fun _substvar_12727_ () Bool)
+(declare-fun _substvar_12728_ () Bool)
+(declare-fun _substvar_12741_ () Bool)
+(declare-fun _substvar_12742_ () Bool)
+(declare-fun _substvar_12747_ () Bool)
+(declare-fun _substvar_12748_ () Bool)
+(declare-fun _substvar_12753_ () Bool)
+(declare-fun _substvar_12754_ () Bool)
+(declare-fun _substvar_12765_ () Bool)
+(declare-fun _substvar_12766_ () Bool)
+(declare-fun _substvar_12791_ () Bool)
+(declare-fun _substvar_12792_ () Bool)
+(declare-fun _substvar_12795_ () Bool)
+(declare-fun _substvar_12796_ () Bool)
+(declare-fun _substvar_12797_ () Bool)
+(declare-fun _substvar_12798_ () Bool)
+(declare-fun _substvar_12811_ () Bool)
+(declare-fun _substvar_12812_ () Bool)
+(declare-fun _substvar_12841_ () Bool)
+(declare-fun _substvar_12842_ () Bool)
+(declare-fun _substvar_12847_ () Bool)
+(declare-fun _substvar_12848_ () Bool)
+(declare-fun _substvar_12853_ () Bool)
+(declare-fun _substvar_12854_ () Bool)
+(declare-fun _substvar_12859_ () Bool)
+(declare-fun _substvar_12860_ () Bool)
+(declare-fun _substvar_12861_ () Bool)
+(declare-fun _substvar_12862_ () Bool)
+(declare-fun _substvar_12873_ () Bool)
+(declare-fun _substvar_12874_ () Bool)
+(declare-fun _substvar_12879_ () Bool)
+(declare-fun _substvar_12880_ () Bool)
+(declare-fun _substvar_12885_ () Bool)
+(declare-fun _substvar_12886_ () Bool)
+(declare-fun _substvar_12893_ () Bool)
+(declare-fun _substvar_12894_ () Bool)
+(declare-fun _substvar_12897_ () Bool)
+(declare-fun _substvar_12898_ () Bool)
+(declare-fun _substvar_12899_ () Bool)
+(declare-fun _substvar_12900_ () Bool)
+(declare-fun _substvar_12903_ () Bool)
+(declare-fun _substvar_12904_ () Bool)
+(declare-fun _substvar_12905_ () Bool)
+(declare-fun _substvar_12906_ () Bool)
+(declare-fun _substvar_12913_ () Bool)
+(declare-fun _substvar_12914_ () Bool)
+(declare-fun _substvar_12917_ () Bool)
+(declare-fun _substvar_12918_ () Bool)
+(declare-fun _substvar_12919_ () Bool)
+(declare-fun _substvar_12920_ () Bool)
+(declare-fun _substvar_12923_ () Bool)
+(declare-fun _substvar_12924_ () Bool)
+(declare-fun _substvar_12929_ () Bool)
+(declare-fun _substvar_12930_ () Bool)
+(declare-fun _substvar_12933_ () Bool)
+(declare-fun _substvar_12934_ () Bool)
+(declare-fun _substvar_12937_ () Bool)
+(declare-fun _substvar_12938_ () Bool)
+(declare-fun _substvar_12969_ () Bool)
+(declare-fun _substvar_12970_ () Bool)
+(declare-fun _substvar_12977_ () Bool)
+(declare-fun _substvar_12978_ () Bool)
+(declare-fun _substvar_12983_ () Bool)
+(declare-fun _substvar_12984_ () Bool)
+(declare-fun _substvar_12997_ () Bool)
+(declare-fun _substvar_12998_ () Bool)
+(declare-fun _substvar_12999_ () Bool)
+(declare-fun _substvar_13000_ () Bool)
+(declare-fun _substvar_13015_ () Bool)
+(declare-fun _substvar_13016_ () Bool)
+(declare-fun _substvar_13021_ () Bool)
+(declare-fun _substvar_13022_ () Bool)
+(declare-fun _substvar_13027_ () Bool)
+(declare-fun _substvar_13028_ () Bool)
+(declare-fun _substvar_13065_ () Bool)
+(declare-fun _substvar_13066_ () Bool)
+(declare-fun _substvar_13071_ () Bool)
+(declare-fun _substvar_13072_ () Bool)
+(declare-fun _substvar_13079_ () Bool)
+(declare-fun _substvar_13080_ () Bool)
+(declare-fun _substvar_13092_ () Bool)
+(declare-fun _substvar_13107_ () Bool)
+(declare-fun _substvar_13116_ () Bool)
+(declare-fun _substvar_13121_ () Bool)
+(declare-fun _substvar_13124_ () Bool)
+(declare-fun _substvar_13129_ () Bool)
+(declare-fun _substvar_13136_ () Bool)
+(declare-fun _substvar_13138_ () Bool)
+(declare-fun _substvar_13140_ () Bool)
+(declare-fun _substvar_13144_ () Bool)
+(declare-fun _substvar_13147_ () Bool)
+(declare-fun _substvar_13148_ () Bool)
+(declare-fun _substvar_13150_ () Bool)
+(declare-fun _substvar_13153_ () Bool)
+(declare-fun _substvar_13155_ () Bool)
+(declare-fun _substvar_13157_ () Bool)
+(declare-fun _substvar_13159_ () Bool)
+(declare-fun _substvar_13160_ () Bool)
+(declare-fun _substvar_13163_ () Bool)
+(declare-fun _substvar_13167_ () Bool)
+(declare-fun _substvar_13168_ () Bool)
+(declare-fun _substvar_13169_ () Bool)
+(declare-fun _substvar_13170_ () Bool)
+(declare-fun _substvar_13171_ () Bool)
+(declare-fun _substvar_13173_ () Bool)
+(declare-fun _substvar_13180_ () Bool)
+(declare-fun _substvar_13181_ () Bool)
+(declare-fun _substvar_13182_ () Bool)
+(declare-fun _substvar_13184_ () Bool)
+(declare-fun _substvar_13187_ () Bool)
+(declare-fun _substvar_13191_ () Bool)
+(declare-fun _substvar_13193_ () Bool)
+(declare-fun _substvar_13194_ () Bool)
+(declare-fun _substvar_13197_ () Bool)
+(declare-fun _substvar_13201_ () Bool)
+(declare-fun _substvar_13207_ () Bool)
+(declare-fun _substvar_13208_ () Bool)
+(declare-fun _substvar_13210_ () Bool)
+(declare-fun _substvar_13219_ () Bool)
+(declare-fun _substvar_13220_ () Bool)
+(declare-fun _substvar_13222_ () Bool)
+(declare-fun _substvar_13225_ () Bool)
+(declare-fun _substvar_13226_ () Bool)
+(declare-fun _substvar_13229_ () Bool)
+(declare-fun _substvar_13230_ () Bool)
+(declare-fun _substvar_13232_ () Bool)
+(declare-fun _substvar_13235_ () Bool)
+(declare-fun _substvar_13236_ () Bool)
+(declare-fun _substvar_13238_ () Bool)
+(declare-fun _substvar_13241_ () Bool)
+(declare-fun _substvar_13242_ () Bool)
+(declare-fun _substvar_13245_ () Bool)
+(declare-fun _substvar_13254_ () Bool)
+(declare-fun _substvar_13255_ () Bool)
+(declare-fun _substvar_13256_ () Bool)
+(declare-fun _substvar_13257_ () Bool)
+(declare-fun _substvar_13262_ () Bool)
+(declare-fun _substvar_13269_ () Bool)
+(declare-fun _substvar_13271_ () Bool)
+(declare-fun _substvar_13283_ () Bool)
+(declare-fun _substvar_13286_ () Bool)
+(declare-fun _substvar_13294_ () Bool)
+(declare-fun _substvar_13297_ () Bool)
+(declare-fun _substvar_13300_ () Bool)
+(declare-fun _substvar_13320_ () Bool)
+(declare-fun _substvar_13322_ () Bool)
+(declare-fun _substvar_13325_ () Bool)
+(declare-fun _substvar_13329_ () Bool)
+(declare-fun _substvar_13330_ () Bool)
+(declare-fun _substvar_13333_ () Bool)
+(declare-fun _substvar_13336_ () Bool)
+(declare-fun _substvar_13339_ () Bool)
+(declare-fun _substvar_13341_ () Bool)
+(declare-fun _substvar_13343_ () Bool)
+(declare-fun _substvar_13347_ () Bool)
+(declare-fun _substvar_13351_ () Bool)
+(declare-fun _substvar_13355_ () Bool)
+(declare-fun _substvar_13357_ () Bool)
+(declare-fun _substvar_13358_ () Bool)
+(declare-fun _substvar_13359_ () Bool)
+(declare-fun _substvar_13360_ () Bool)
+(declare-fun _substvar_13367_ () Bool)
+(declare-fun _substvar_13368_ () Bool)
+(declare-fun _substvar_13369_ () Bool)
+(declare-fun _substvar_13370_ () Bool)
+(declare-fun _substvar_13375_ () Bool)
+(declare-fun _substvar_13378_ () Bool)
+(declare-fun _substvar_13380_ () Bool)
+(declare-fun _substvar_13383_ () Bool)
+(declare-fun _substvar_13413_ () Bool)
+(declare-fun _substvar_13415_ () Bool)
+(declare-fun _substvar_13416_ () Bool)
+(declare-fun _substvar_13419_ () Bool)
+(declare-fun _substvar_13423_ () Bool)
+(declare-fun _substvar_13427_ () Bool)
+(declare-fun _substvar_13430_ () Bool)
+(declare-fun _substvar_13433_ () Bool)
+(declare-fun _substvar_13434_ () Bool)
+(declare-fun _substvar_13437_ () Bool)
+(declare-fun _substvar_13444_ () Bool)
+(declare-fun _substvar_13446_ () Bool)
+(declare-fun _substvar_13449_ () Bool)
+(declare-fun _substvar_13450_ () Bool)
+(declare-fun _substvar_13453_ () Bool)
+(declare-fun _substvar_13454_ () Bool)
+(declare-fun _substvar_13456_ () Bool)
+(declare-fun _substvar_13458_ () Bool)
+(declare-fun _substvar_13461_ () Bool)
+(declare-fun _substvar_13462_ () Bool)
+(declare-fun _substvar_13466_ () Bool)
+(declare-fun _substvar_13476_ () Bool)
+(declare-fun _substvar_13477_ () Bool)
+(declare-fun _substvar_13478_ () Bool)
+(declare-fun _substvar_13479_ () Bool)
+(declare-fun _substvar_13482_ () Bool)
+(declare-fun _substvar_13486_ () Bool)
+(declare-fun _substvar_13487_ () Bool)
+(declare-fun _substvar_13488_ () Bool)
+(declare-fun _substvar_13489_ () Bool)
+(declare-fun _substvar_13490_ () Bool)
+(declare-fun _substvar_13491_ () Bool)
+(declare-fun _substvar_13504_ () Bool)
+(declare-fun _substvar_13508_ () Bool)
+(declare-fun _substvar_18407_ () Bool)
+(declare-fun _substvar_18409_ () Bool)
+(declare-fun _substvar_18424_ () Bool)
+(declare-fun _substvar_18448_ () Bool)
+(declare-fun _substvar_18450_ () Bool)
+(declare-fun _substvar_18452_ () Bool)
+(declare-fun _substvar_18455_ () Bool)
+(declare-fun _substvar_18457_ () Bool)
+(declare-fun _substvar_18459_ () Bool)
+(declare-fun _substvar_18461_ () Bool)
+(declare-fun _substvar_18467_ () Bool)
+(declare-fun _substvar_18470_ () Bool)
+(declare-fun _substvar_18472_ () Bool)
+(declare-fun _substvar_18474_ () Bool)
+(declare-fun _substvar_18476_ () Bool)
+(declare-fun _substvar_18478_ () Bool)
+(declare-fun _substvar_18480_ () Bool)
+(declare-fun _substvar_18482_ () Bool)
+(declare-fun _substvar_21042_ () Bool)
+(declare-fun _substvar_21097_ () Bool)
+(declare-fun _substvar_21140_ () Bool)
+(declare-fun _substvar_21181_ () Bool)
+(declare-fun _substvar_21205_ () Bool)
+(declare-fun _substvar_21216_ () Bool)
+(declare-fun _substvar_21219_ () Bool)
+(declare-fun _substvar_21222_ () Bool)
+(declare-fun _substvar_21236_ () Bool)
+(declare-fun _substvar_21305_ () Bool)
+(declare-fun _substvar_25332_ () Bool)
+(declare-fun _substvar_25333_ () Bool)
+(declare-fun _substvar_25567_ () Bool)
+(declare-fun _substvar_25569_ () Bool)
+(declare-fun _substvar_25575_ () Bool)
+(declare-fun _substvar_25604_ () Bool)
+(declare-fun _substvar_25733_ () Bool)
+(declare-sort FArray 2)
+(declare-fun f139 () Int)
+(declare-fun f138 () Int)
+(declare-fun f137 () Int)
+(declare-fun f136 () Int)
+(declare-fun f135 () Int)
+(declare-fun f134 () Int)
+(declare-fun f133 () Int)
+(declare-fun f132 () Int)
+(declare-fun f131 () Int)
+(declare-fun f130 () Int)
+(declare-fun f129 () Int)
+(declare-fun f128 () Int)
+(declare-fun f127 () Int)
+(declare-fun f126 () Int)
+(declare-fun f125 () Int)
+(declare-fun f124 () Int)
+(declare-fun f123 () Int)
+(declare-fun f122 () Int)
+(declare-fun f121 () Int)
+(declare-fun f120 () Int)
+(declare-fun f119 () Int)
+(declare-fun f118 () Int)
+(declare-fun f117 () Int)
+(declare-fun f116 () Int)
+(declare-fun f115 () Int)
+(declare-fun f114 () Int)
+(declare-fun f113 () Int)
+(declare-fun f112 () Int)
+(declare-fun f111 () Int)
+(declare-fun f110 () Int)
+(declare-fun f109 () Int)
+(declare-fun f88@0 () Bool)
+(declare-fun f89@0 () Bool)
+(declare-fun f90@0 () Bool)
+(declare-fun f91@0 () Bool)
+(declare-fun f92@0 () Bool)
+(declare-fun f93@0 () Bool)
+(declare-fun f94@0 () Bool)
+(declare-fun f95@0 () Bool)
+(declare-fun f96@0 () Bool)
+(declare-fun f97@0 () Bool)
+(declare-fun f98@0 () Bool)
+(declare-fun f99@0 () Bool)
+(declare-fun f100@0 () Int)
+(declare-fun f101@0 () Bool)
+(declare-fun f86@0 () Bool)
+(declare-fun f140@0 () Int)
+(declare-fun f141@0 () Int)
+(declare-fun f142@0 () Int)
+(declare-fun f143@0 () Int)
+(declare-fun f144@0 () Int)
+(declare-fun f145@0 () Bool)
+(declare-fun f146@0 () Bool)
+(declare-fun f147@0 () Bool)
+(declare-fun f148@0 () Bool)
+(declare-fun f152@0 () Bool)
+(declare-fun f151@0 () Int)
+(declare-fun f150@0 () Bool)
+(declare-fun f149@0 () Bool)
+(declare-fun f88@1 () Bool)
+(declare-fun f89@1 () Bool)
+(declare-fun f90@1 () Bool)
+(declare-fun f91@1 () Bool)
+(declare-fun f92@1 () Bool)
+(declare-fun f93@1 () Bool)
+(declare-fun f94@1 () Bool)
+(declare-fun f95@1 () Bool)
+(declare-fun f96@1 () Bool)
+(declare-fun f97@1 () Bool)
+(declare-fun f98@1 () Bool)
+(declare-fun f99@1 () Bool)
+(declare-fun f100@1 () Int)
+(declare-fun f101@1 () Bool)
+(declare-fun f86@1 () Bool)
+(declare-fun f140@1 () Int)
+(declare-fun f141@1 () Int)
+(declare-fun f142@1 () Int)
+(declare-fun f143@1 () Int)
+(declare-fun f144@1 () Int)
+(declare-fun f145@1 () Bool)
+(declare-fun f146@1 () Bool)
+(declare-fun f147@1 () Bool)
+(declare-fun f148@1 () Bool)
+(declare-fun f152@1 () Bool)
+(declare-fun f151@1 () Int)
+(declare-fun f150@1 () Bool)
+(declare-fun f149@1 () Bool)
+(declare-fun __ic3_frame_0 () Bool)
+(declare-fun __ic3_clause_1_n0_0 () Bool)
+(declare-fun __ic3_clause_2_n1_0 () Bool)
+(declare-fun __ic3_clause_2_p0 () Bool)
+(assert (=> _substvar_12544_ (and (= _substvar_10022_ (and _substvar_10021_ (> _substvar_577_ 0))) (= _substvar_10018_ (=> _substvar_13092_ _substvar_21042_)) (and (= _substvar_578_ 0) (= _substvar_579_ 0) (= _substvar_580_ 0) (= _substvar_581_ 0) (= _substvar_583_ _substvar_577_) (= _substvar_582_ _substvar_583_) (= _substvar_5910_ _substvar_5919_) _substvar_5911_) (and (= _substvar_10023_ _substvar_10022_) _substvar_7336_) (and (= _substvar_4550_ (or (or (or (or (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and _substvar_6010_ _substvar_6011_) _substvar_6730_) _substvar_6732_) _substvar_6734_) _substvar_6736_) _substvar_6738_) _substvar_6740_) _substvar_6742_) _substvar_6744_) _substvar_6746_) _substvar_6748_) (and (and (and (and (and (and (and (and (and (and (and _substvar_6728_ _substvar_6750_) _substvar_6752_) _substvar_6754_) _substvar_6756_) _substvar_6758_) _substvar_6760_) _substvar_6762_) _substvar_6764_) _substvar_6766_) _substvar_6768_) _substvar_6770_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6773_ _substvar_6008_) _substvar_6775_) _substvar_6777_) _substvar_6779_) _substvar_6781_) _substvar_6783_) _substvar_6785_) _substvar_6787_) _substvar_6789_) _substvar_6791_) _substvar_6793_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6796_ _substvar_6797_) _substvar_4540_) _substvar_6800_) _substvar_6802_) _substvar_6804_) _substvar_6806_) _substvar_6808_) _substvar_6810_) _substvar_6812_) _substvar_6814_) _substvar_6816_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6102_ _substvar_6103_) _substvar_6820_) _substvar_4541_) _substvar_6823_) _substvar_6825_) _substvar_6827_) _substvar_6829_) _substvar_6831_) _substvar_6833_) _substvar_6835_) _substvar_6837_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6840_ _substvar_6841_) _substvar_6843_) _substvar_6845_) _substvar_4542_) _substvar_6848_) _substvar_6850_) _substvar_6852_) _substvar_6854_) _substvar_6856_) _substvar_6858_) _substvar_6860_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6148_ _substvar_6149_) _substvar_6864_) _substvar_6866_) _substvar_6868_) _substvar_4543_) _substvar_6871_) _substvar_6873_) _substvar_6875_) _substvar_6877_) _substvar_6879_) _substvar_6881_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6884_ _substvar_6885_) _substvar_6887_) _substvar_6889_) _substvar_6891_) _substvar_6893_) _substvar_4544_) _substvar_6896_) _substvar_6898_) _substvar_6900_) _substvar_6902_) _substvar_6904_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6194_ _substvar_6195_) _substvar_6908_) _substvar_6910_) _substvar_6912_) _substvar_6914_) _substvar_6916_) _substvar_4545_) _substvar_6919_) _substvar_6921_) _substvar_6923_) _substvar_6925_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6928_ _substvar_6929_) _substvar_6931_) _substvar_6933_) _substvar_6935_) _substvar_6937_) _substvar_6939_) _substvar_6941_) _substvar_4546_) _substvar_6944_) _substvar_6946_) _substvar_6948_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6240_ _substvar_6241_) _substvar_6952_) _substvar_6954_) _substvar_6956_) _substvar_6958_) _substvar_6960_) _substvar_6962_) _substvar_6964_) _substvar_4547_) _substvar_6967_) _substvar_6969_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6972_ _substvar_6973_) _substvar_6975_) _substvar_6977_) _substvar_6979_) _substvar_6981_) _substvar_6983_) _substvar_6985_) _substvar_6987_) _substvar_6989_) _substvar_4548_) _substvar_6992_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_6286_ _substvar_6287_) _substvar_6996_) _substvar_6998_) _substvar_7000_) _substvar_7002_) _substvar_7004_) _substvar_7006_) _substvar_7008_) _substvar_7010_) _substvar_7012_) _substvar_4549_))) _substvar_6009_) _substvar_10019_)))
+(assert (let ((_let_0 (>= _substvar_582_ 1))) (let ((_let_1 (and (and (and (and _let_0 (= _substvar_581_ 0)) (= _substvar_579_ 0)) (= _substvar_578_ 0)) (= _substvar_580_ 0)))) (let ((_let_2 (- _substvar_581_ 1))) (let ((_let_3 (and _let_0 (>= (+ (- (+ _let_2 _substvar_579_) _substvar_578_) _substvar_580_) 1)))) (let ((_let_4 (- _substvar_578_ 1))) (let ((_let_5 (and _substvar_6661_ (>= (+ (+ (+ _substvar_581_ _substvar_579_) _substvar_578_) _substvar_580_) 1)))) (let ((_let_6 (+ _substvar_579_ _substvar_578_))) (let ((_let_7 (and _substvar_6685_ (= _substvar_579_ 1)))) (let ((_let_8 (>= (+ _substvar_580_ _substvar_579_) 2))) (let ((_let_9 (>= _substvar_579_ 1))) (let ((_let_10 (and (= _substvar_580_ 1) _substvar_6692_))) (let ((_let_11 (>= _substvar_580_ 1))) (let ((_let_12 (+ _substvar_581_ 1))) (let ((_let_13 (>= _substvar_581_ 1))) (let ((_let_15 (+ _substvar_582_ 1))) (and (= _substvar_10043_ (and _substvar_10042_ _substvar_13107_)) (= _substvar_10039_ (=> _substvar_10044_ (<= _substvar_857_ 1))) (and (= _substvar_584_ (ite _substvar_10027_ (ite _let_1 (+ _substvar_578_ 1) _substvar_578_) (ite _substvar_10028_ (ite _let_3 0 _substvar_578_) (ite _substvar_10029_ _let_4 (ite _substvar_10034_ (ite _let_5 0 _substvar_578_) (ite _substvar_10038_ (ite _substvar_25333_ _let_4 _substvar_578_) _substvar_578_)))))) (= _substvar_585_ (ite _substvar_10028_ (ite _let_3 0 _substvar_579_) (ite _substvar_10031_ (ite _let_7 0 _substvar_579_) (ite _substvar_10032_ (ite _let_8 0 _substvar_579_) (ite _substvar_10034_ (ite _let_5 (+ (+ _let_6 _substvar_580_) _substvar_581_) _substvar_579_) (ite _substvar_10036_ (ite _let_9 0 _substvar_579_) _substvar_579_)))))) (= _substvar_856_ (ite _substvar_10028_ (ite _let_3 0 _substvar_580_) (ite _substvar_10030_ (ite _let_10 0 _substvar_580_) (ite _substvar_10032_ (ite _let_8 1 _substvar_580_) (ite _substvar_10034_ (ite _let_5 1 _substvar_580_) (ite _substvar_10037_ (ite _let_11 0 _substvar_580_) _substvar_580_)))))) (= _substvar_857_ (ite _substvar_10028_ (ite _let_3 0 _substvar_581_) (ite _substvar_10029_ (ite (>= _substvar_578_ 1) _let_12 _substvar_581_) (ite _substvar_10030_ (ite _let_10 _let_12 _substvar_581_) (ite _substvar_10031_ (ite _let_7 _let_12 _substvar_581_) (ite _substvar_10033_ (ite _let_1 _let_12 _substvar_581_) (ite _substvar_10034_ (ite _let_5 0 _substvar_581_) (ite _substvar_10035_ (ite _let_13 _let_2 _substvar_581_) _substvar_581_)))))))) (= _substvar_991_ (ite _substvar_10027_ _substvar_875_ (ite _substvar_10028_ (ite _let_3 _substvar_875_ _substvar_582_) (ite _substvar_10033_ (ite _let_1 _substvar_875_ _substvar_582_) (ite _substvar_10034_ (ite _let_5 _substvar_875_ _substvar_582_) (ite _substvar_10035_ (ite _let_13 _let_15 _substvar_582_) (ite _substvar_10036_ (ite _let_9 _let_15 _substvar_582_) (ite _substvar_10037_ (ite _let_11 _let_15 _substvar_582_) (ite _substvar_10038_ (ite _substvar_25333_ _let_15 _substvar_582_) _substvar_582_))))))))) _substvar_6712_ (= _substvar_5934_ _substvar_5991_) _substvar_6714_) (and (= _substvar_10044_ (and _substvar_10043_ _substvar_10023_)) _substvar_7344_) (and (= _substvar_10042_ (or (or (or (or (or (or (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_25567_) _substvar_25569_) _substvar_18407_) _substvar_18409_) (not _substvar_10032_)) _substvar_25575_) (not _substvar_10034_)) _substvar_7047_) (not _substvar_10036_)) (not _substvar_10037_)) (not _substvar_10038_)) (and (and (and (and (and (and (and (and (and (and (and _substvar_10027_ _substvar_18424_) (not _substvar_10029_)) (not _substvar_10030_)) (not _substvar_10031_)) (not _substvar_10032_)) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) _substvar_7071_) (not _substvar_10037_)) _substvar_25604_)) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_10028_) _substvar_18448_) _substvar_18450_) _substvar_18452_) _substvar_7086_) _substvar_18455_) _substvar_18457_) _substvar_18459_) _substvar_18461_) _substvar_7096_) _substvar_7098_)) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_18467_) _substvar_10029_) _substvar_18470_) _substvar_18472_) _substvar_18474_) _substvar_18476_) _substvar_18478_) _substvar_18480_) _substvar_18482_) _substvar_7119_) _substvar_7121_)) (and (and (and (and (and (and (and (and (and _substvar_7128_ _substvar_10030_) (not _substvar_10031_)) (not _substvar_10032_)) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) (not _substvar_10036_)) _substvar_7142_) _substvar_7144_)) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7148_) _substvar_7150_) _substvar_7152_) _substvar_10031_) (not _substvar_10032_)) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) (not _substvar_10036_)) (not _substvar_10037_)) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7171_) _substvar_7173_) _substvar_7175_) _substvar_7177_) _substvar_10032_) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) (not _substvar_10036_)) (not _substvar_10037_)) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7194_) _substvar_7196_) _substvar_7198_) _substvar_7200_) (not _substvar_10032_)) _substvar_10033_) (not _substvar_10034_)) (not _substvar_10035_)) (not _substvar_10036_)) (not _substvar_10037_)) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7217_) _substvar_7219_) _substvar_7221_) _substvar_7223_) (not _substvar_10032_)) (not _substvar_10033_)) _substvar_10034_) (not _substvar_10035_)) (not _substvar_10036_)) (not _substvar_10037_)) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7240_) _substvar_7242_) _substvar_7244_) _substvar_7246_) (not _substvar_10032_)) _substvar_25733_) (not _substvar_10034_)) _substvar_10035_) (not _substvar_10036_)) (not _substvar_10037_)) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7263_) _substvar_7265_) _substvar_7267_) _substvar_7269_) (not _substvar_10032_)) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) _substvar_10036_) (not _substvar_10037_)) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7286_) _substvar_7288_) _substvar_7290_) _substvar_7292_) (not _substvar_10032_)) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) _substvar_7302_) _substvar_10037_) (not _substvar_10038_))) (and (and (and (and (and (and (and (and (and (and (and (not _substvar_10027_) _substvar_7309_) _substvar_7311_) _substvar_7313_) _substvar_7315_) _substvar_7317_) (not _substvar_10033_)) (not _substvar_10034_)) (not _substvar_10035_)) _substvar_7325_) _substvar_7327_) _substvar_10038_))) _substvar_7332_) _substvar_13116_)))))))))))))))))
+(assert (=> _substvar_12573_ _substvar_12574_))
+(assert (=> _substvar_13121_ (not _substvar_10039_)))
+(assert (=> _substvar_13124_ _substvar_10018_))
+(declare-fun termITE_1 () Int)
+(declare-fun termITE_2 () Int)
+(declare-fun termITE_3 () Int)
+(declare-fun termITE_4 () Int)
+(declare-fun termITE_5 () Int)
+(declare-fun termITE_6 () Int)
+(declare-fun termITE_7 () Int)
+(declare-fun termITE_8 () Int)
+(declare-fun termITE_9 () Int)
+(declare-fun termITE_10 () Int)
+(declare-fun termITE_11 () Int)
+(declare-fun termITE_12 () Int)
+(declare-fun termITE_13 () Int)
+(declare-fun termITE_14 () Int)
+(declare-fun termITE_15 () Int)
+(declare-fun termITE_16 () Int)
+(declare-fun termITE_17 () Int)
+(declare-fun termITE_18 () Int)
+(declare-fun termITE_19 () Int)
+(declare-fun termITE_20 () Int)
+(declare-fun termITE_21 () Int)
+(declare-fun termITE_22 () Int)
+(declare-fun termITE_23 () Int)
+(declare-fun termITE_24 () Int)
+(declare-fun termITE_25 () Int)
+(declare-fun termITE_26 () Int)
+(declare-fun termITE_27 () Int)
+(declare-fun termITE_28 () Int)
+(declare-fun termITE_29 () Int)
+(declare-fun termITE_30 () Int)
+(declare-fun termITE_31 () Int)
+(declare-fun termITE_32 () Int)
+(declare-fun termITE_33 () Int)
+(declare-fun termITE_34 () Int)
+(declare-fun termITE_35 () Int)
+(declare-fun termITE_36 () Int)
+(declare-fun termITE_37 () Int)
+(declare-fun termITE_38 () Int)
+(declare-fun termITE_39 () Int)
+(declare-fun termITE_40 () Int)
+(declare-fun termITE_41 () Int)
+(declare-fun termITE_42 () Int)
+(declare-fun termITE_43 () Int)
+(declare-fun termITE_44 () Int)
+(declare-fun termITE_45 () Int)
+(declare-fun termITE_46 () Int)
+(declare-fun termITE_47 () Int)
+(declare-fun termITE_48 () Int)
+(declare-fun termITE_49 () Int)
+(declare-fun termITE_50 () Int)
+(declare-fun termITE_51 () Int)
+(declare-fun termITE_52 () Int)
+(declare-fun termITE_53 () Int)
+(declare-fun termITE_54 () Int)
+(declare-fun termITE_55 () Int)
+(declare-fun termITE_56 () Int)
+(declare-fun termITE_57 () Int)
+(declare-fun termITE_58 () Int)
+(push 1)
+(declare-fun c2 () Bool)
+(declare-fun c4 () Bool)
+(assert _substvar_12544_)
+(assert _substvar_13121_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_3_n0_0 () Bool)
+(assert (=> _substvar_12583_ _substvar_12584_))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_check_frames_0 () Bool)
+(assert (=> _substvar_13129_ (not _substvar_10039_)))
+(push 1)
+(declare-fun c6 () Bool)
+(declare-fun c7 () Bool)
+(assert _substvar_13129_)
+(assert _substvar_12544_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_3_n1_0 () Bool)
+(declare-fun __ic3_clause_3_p0 () Bool)
+(assert (=> _substvar_12592_ (not _substvar_10039_)))
+(assert (=> _substvar_13136_ _substvar_10018_))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_4_n1_0 () Bool)
+(declare-fun __ic3_clause_4_n1_1 () Bool)
+(declare-fun __ic3_clause_4_n1_2 () Bool)
+(declare-fun __ic3_clause_4_n1_3 () Bool)
+(declare-fun __ic3_clause_4_n1_4 () Bool)
+(declare-fun __ic3_clause_4_p0 () Bool)
+(assert (=> _substvar_13138_ _substvar_10039_))
+(assert (=> _substvar_13140_ (not (= (+ (* (- 1) _substvar_857_) 0) 0))))
+(assert (=> _substvar_13144_ _substvar_10044_))
+(assert (=> _substvar_12605_ _substvar_12606_))
+(assert (=> _substvar_13147_ _substvar_13148_))
+(assert (=> _substvar_12611_ (or _substvar_12612_ _substvar_11989_ _substvar_11990_ _substvar_11992_ _substvar_13150_)))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_4_n0_0 () Bool)
+(declare-fun __ic3_clause_4_n0_1 () Bool)
+(declare-fun __ic3_clause_4_n0_2 () Bool)
+(declare-fun __ic3_clause_4_n0_3 () Bool)
+(declare-fun __ic3_clause_4_n0_4 () Bool)
+(assert (=> _substvar_13153_ _substvar_10018_))
+(assert (=> _substvar_13155_ _substvar_12620_))
+(assert (=> _substvar_13157_ _substvar_10023_))
+(assert (=> _substvar_13159_ _substvar_13160_))
+(assert (=> _substvar_12627_ _substvar_12628_))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_0 () Bool)
+(declare-fun __ic3_ind_gen_1 () Bool)
+(declare-fun __ic3_ind_gen_2 () Bool)
+(assert (=> _substvar_13163_ (not (or _substvar_12632_ _substvar_12633_ _substvar_12634_))))
+(assert (=> _substvar_13167_ _substvar_12644_))
+(assert (=> _substvar_13173_ (or _substvar_12648_ _substvar_12649_ _substvar_12650_)))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_3 () Bool)
+(declare-fun __ic3_ind_gen_4 () Bool)
+(declare-fun __ic3_ind_gen_5 () Bool)
+(assert (=> _substvar_12037_ (not (or _substvar_12038_ _substvar_21097_))))
+(assert (=> _substvar_13180_ _substvar_13182_))
+(assert (=> _substvar_12663_ (or _substvar_12664_ _substvar_13184_)))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_6 () Bool)
+(declare-fun __ic3_ind_gen_7 () Bool)
+(declare-fun __ic3_ind_gen_8 () Bool)
+(assert (=> _substvar_12671_ (not (or _substvar_12673_ _substvar_12674_))))
+(assert (=> _substvar_12064_ _substvar_13191_))
+(assert (=> _substvar_13193_ (or _substvar_12682_ _substvar_13194_)))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_9 () Bool)
+(declare-fun __ic3_ind_gen_10 () Bool)
+(declare-fun __ic3_ind_gen_11 () Bool)
+(assert (=> _substvar_12688_ (> (+ (* 1 _substvar_857_) (- 1)) 0)))
+(assert (=> _substvar_12691_ _substvar_12692_))
+(assert (=> _substvar_13201_ _substvar_12696_))
+(push 1)
+(declare-fun c41 () Bool)
+(assert _substvar_12688_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_5_p0 () Bool)
+(assert (=> _substvar_12700_ (not (> (+ (* 1 _substvar_581_) (- 1)) 0))))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_5_n0_0 () Bool)
+(declare-fun __ic3_check_frames_1 () Bool)
+(assert (=> _substvar_13207_ _substvar_13208_))
+(assert (let ((_let_0 (not (> (+ (* 1 _substvar_857_) (- 1)) 0)))) (=> _substvar_13210_ (not (and _substvar_10039_ _let_0 _let_0)))))
+(push 1)
+(declare-fun c48 () Bool)
+(assert _substvar_13210_)
+(check-sat)
+(pop 1)
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_6_n1_0 () Bool)
+(declare-fun __ic3_clause_6_n1_1 () Bool)
+(declare-fun __ic3_clause_6_n1_2 () Bool)
+(declare-fun __ic3_clause_6_n1_3 () Bool)
+(declare-fun __ic3_clause_6_n1_4 () Bool)
+(declare-fun __ic3_clause_6_n1_5 () Bool)
+(declare-fun __ic3_clause_6_p0 () Bool)
+(assert (=> _substvar_13220_ _substvar_10039_))
+(assert (=> _substvar_13222_ _substvar_10044_))
+(assert (=> _substvar_12721_ _substvar_12722_))
+(assert (=> _substvar_13225_ _substvar_13226_))
+(assert (=> _substvar_12727_ _substvar_12728_))
+(assert (=> _substvar_13229_ _substvar_13230_))
+(assert (=> _substvar_12124_ (or _substvar_12125_ _substvar_12126_ _substvar_12128_ _substvar_12130_ _substvar_12132_ _substvar_13232_)))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_6_n0_0 () Bool)
+(declare-fun __ic3_clause_6_n0_1 () Bool)
+(declare-fun __ic3_clause_6_n0_2 () Bool)
+(declare-fun __ic3_clause_6_n0_3 () Bool)
+(declare-fun __ic3_clause_6_n0_4 () Bool)
+(declare-fun __ic3_clause_6_n0_5 () Bool)
+(assert (=> _substvar_13236_ _substvar_10018_))
+(assert (=> _substvar_13238_ _substvar_10023_))
+(assert (=> _substvar_12741_ _substvar_12742_))
+(assert (=> _substvar_13241_ _substvar_13242_))
+(assert (=> _substvar_12747_ _substvar_12748_))
+(assert (=> _substvar_13245_ _substvar_21140_))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_12 () Bool)
+(declare-fun __ic3_ind_gen_13 () Bool)
+(declare-fun __ic3_ind_gen_14 () Bool)
+(assert (=> _substvar_12754_ (not (or (not (> (* 1 _substvar_857_) 0)) (not _substvar_10044_)))))
+(assert (=> _substvar_13254_ _substvar_12766_))
+(assert (=> _substvar_12169_ _substvar_12173_))
+(push 1)
+(declare-fun c72 () Bool)
+(declare-fun c73 () Bool)
+(assert _substvar_12754_)
+(assert _substvar_12544_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_15 () Bool)
+(declare-fun __ic3_ind_gen_16 () Bool)
+(declare-fun __ic3_ind_gen_17 () Bool)
+(assert (=> _substvar_13262_ (not (or (not (> (* 1 _substvar_584_) 0)) (not _substvar_10044_)))))
+(assert (=> _substvar_12184_ _substvar_13269_))
+(assert (=> _substvar_13271_ (or (not (> (* 1 _substvar_578_) 0)) (not _substvar_10023_))))
+(push 1)
+(declare-fun c77 () Bool)
+(declare-fun c78 () Bool)
+(assert _substvar_13271_)
+(assert _substvar_13262_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_18 () Bool)
+(declare-fun __ic3_ind_gen_19 () Bool)
+(declare-fun __ic3_ind_gen_20 () Bool)
+(assert (=> _substvar_12199_ (not (or _substvar_12201_ _substvar_12203_))))
+(assert (=> _substvar_12791_ _substvar_12213_))
+(assert (=> _substvar_13283_ (or _substvar_12796_ _substvar_12798_)))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_7_p0 () Bool)
+(assert (=> _substvar_13286_ (or (not _substvar_10023_) (not (> (* 1 _substvar_581_) 0)) (not (> (* 1 _substvar_578_) 0)))))
+(push 1)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_7_n0_0 () Bool)
+(declare-fun __ic3_clause_7_n0_1 () Bool)
+(declare-fun __ic3_clause_7_n0_2 () Bool)
+(declare-fun __ic3_check_frames_2 () Bool)
+(declare-fun __ic3_clause_8_n1_0 () Bool)
+(declare-fun __ic3_clause_8_n1_1 () Bool)
+(declare-fun __ic3_clause_8_n1_2 () Bool)
+(declare-fun __ic3_clause_8_n1_3 () Bool)
+(declare-fun __ic3_clause_8_n1_4 () Bool)
+(declare-fun __ic3_clause_8_n1_5 () Bool)
+(declare-fun __ic3_clause_8_n1_6 () Bool)
+(declare-fun __ic3_clause_8_n1_7 () Bool)
+(declare-fun __ic3_clause_8_p0 () Bool)
+(declare-fun __ic3_clause_8_n0_0 () Bool)
+(declare-fun __ic3_clause_8_n0_1 () Bool)
+(declare-fun __ic3_clause_8_n0_2 () Bool)
+(declare-fun __ic3_clause_8_n0_3 () Bool)
+(declare-fun __ic3_clause_8_n0_4 () Bool)
+(declare-fun __ic3_clause_8_n0_5 () Bool)
+(declare-fun __ic3_clause_8_n0_6 () Bool)
+(declare-fun __ic3_clause_8_n0_7 () Bool)
+(declare-fun __ic3_ind_gen_21 () Bool)
+(declare-fun __ic3_ind_gen_22 () Bool)
+(declare-fun __ic3_ind_gen_23 () Bool)
+(declare-fun __ic3_ind_gen_24 () Bool)
+(declare-fun __ic3_ind_gen_25 () Bool)
+(declare-fun __ic3_ind_gen_26 () Bool)
+(declare-fun __ic3_ind_gen_27 () Bool)
+(declare-fun __ic3_ind_gen_28 () Bool)
+(declare-fun __ic3_ind_gen_29 () Bool)
+(declare-fun __ic3_clause_9_p0 () Bool)
+(declare-fun __ic3_clause_9_n0_0 () Bool)
+(declare-fun __ic3_check_frames_3 () Bool)
+(assert (=> _substvar_13294_ _substvar_10023_))
+(assert (=> _substvar_12811_ _substvar_12812_))
+(assert (=> _substvar_13297_ _substvar_21181_))
+(assert (let ((_let_0 (* 1 _substvar_857_))) (let ((_let_1 (not (> _substvar_1089_ 0)))) (let ((_let_2 (or (not _substvar_10044_) (not (> _let_0 0)) (not (> (* 1 _substvar_584_) 0))))) (=> _substvar_13300_ (not (and _substvar_10039_ _let_2 _let_1 _let_2 _let_1)))))))
+(assert (=> _substvar_13320_ _substvar_10039_))
+(assert (=> _substvar_13322_ _substvar_10044_))
+(assert (=> _substvar_12841_ _substvar_12842_))
+(assert (=> _substvar_13325_ _substvar_21205_))
+(assert (=> _substvar_12847_ _substvar_12848_))
+(assert (=> _substvar_13329_ _substvar_13330_))
+(assert (=> _substvar_12853_ _substvar_12854_))
+(assert (=> _substvar_13333_ (= (+ (* (- 1) _substvar_856_) 0) 0)))
+(assert (=> _substvar_12859_ (or _substvar_12860_ _substvar_12861_ _substvar_12284_ _substvar_12286_ _substvar_12288_ _substvar_12290_ _substvar_12292_ _substvar_13336_)))
+(assert (=> _substvar_13339_ _substvar_10018_))
+(assert (=> _substvar_13341_ _substvar_10023_))
+(assert (=> _substvar_13343_ _substvar_21216_))
+(assert (=> _substvar_12873_ _substvar_12874_))
+(assert (=> _substvar_13347_ _substvar_21219_))
+(assert (=> _substvar_12879_ _substvar_12880_))
+(assert (=> _substvar_13351_ _substvar_21222_))
+(assert (=> _substvar_12885_ _substvar_12886_))
+(assert (=> _substvar_12319_ _substvar_13355_))
+(assert (=> _substvar_13357_ _substvar_13360_))
+(assert (=> _substvar_12897_ (or _substvar_12899_ _substvar_12900_)))
+(assert (=> _substvar_12903_ (not (or _substvar_12905_ _substvar_12906_))))
+(assert (=> _substvar_13367_ _substvar_13370_))
+(assert (=> _substvar_12917_ (or _substvar_12919_ _substvar_12920_)))
+(assert (=> _substvar_12923_ _substvar_12924_))
+(assert (=> _substvar_13375_ _substvar_21236_))
+(assert (=> _substvar_12929_ _substvar_13378_))
+(assert (=> _substvar_12933_ _substvar_13380_))
+(assert (=> _substvar_12937_ _substvar_12938_))
+(assert (let ((_let_0 (* 1 _substvar_857_))) (let ((_let_1 (not (> (+ _let_0 (- 1)) 0)))) (let ((_let_2 (or (not _substvar_10044_) (not (> _let_0 0)) (not (> (* 1 _substvar_584_) 0))))) (let ((_let_3 (not (= (+ (* (- 1) _substvar_585_) 1) 0)))) (=> _substvar_13383_ (not (and _substvar_10039_ _let_2 _let_1 _let_3 _let_2 _let_1 _let_3))))))))
+(push 1)
+(declare-fun c155 () Bool)
+(declare-fun c156 () Bool)
+(assert _substvar_13383_)
+(assert _substvar_12544_)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun c158 () Bool)
+(declare-fun c159 () Bool)
+(declare-fun c160 () Bool)
+(assert _substvar_12592_)
+(assert _substvar_13286_)
+(assert _substvar_12700_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_10_n1_0 () Bool)
+(declare-fun __ic3_clause_10_n1_1 () Bool)
+(declare-fun __ic3_clause_10_n1_2 () Bool)
+(declare-fun __ic3_clause_10_n1_3 () Bool)
+(declare-fun __ic3_clause_10_n1_4 () Bool)
+(declare-fun __ic3_clause_10_n1_5 () Bool)
+(declare-fun __ic3_clause_10_n1_6 () Bool)
+(declare-fun __ic3_clause_10_n1_7 () Bool)
+(declare-fun __ic3_clause_10_n1_8 () Bool)
+(declare-fun __ic3_clause_10_p0 () Bool)
+(assert (=> _substvar_12970_ _substvar_10039_))
+(assert (=> _substvar_13413_ _substvar_10044_))
+(assert (=> _substvar_13415_ _substvar_13416_))
+(assert (=> _substvar_12977_ _substvar_12978_))
+(assert (=> _substvar_13419_ (> (* 1 _substvar_857_) 0)))
+(assert (=> _substvar_12983_ _substvar_12984_))
+(assert (=> _substvar_13423_ (not (= (+ (* 1 _substvar_585_) (- 1)) 0))))
+(assert (=> _substvar_13427_ (= (+ (* (- 1) _substvar_856_) 1) 0)))
+(assert (=> _substvar_13430_ (= (+ (* (- 1) _substvar_585_) 0) 0)))
+(assert (=> _substvar_13433_ (or _substvar_12997_ _substvar_12434_ _substvar_12436_ _substvar_12438_ _substvar_12440_ _substvar_12442_ _substvar_12443_ _substvar_12999_ _substvar_13434_)))
+(push 1)
+(declare-fun c164 () Bool)
+(declare-fun c167 () Bool)
+(declare-fun c169 () Bool)
+(declare-fun c170 () Bool)
+(declare-fun c171 () Bool)
+(declare-fun c172 () Bool)
+(assert _substvar_13413_)
+(assert _substvar_13419_)
+(assert _substvar_13423_)
+(assert _substvar_13427_)
+(assert _substvar_13430_)
+(assert _substvar_12544_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_clause_10_n0_0 () Bool)
+(declare-fun __ic3_clause_10_n0_1 () Bool)
+(declare-fun __ic3_clause_10_n0_2 () Bool)
+(declare-fun __ic3_clause_10_n0_3 () Bool)
+(declare-fun __ic3_clause_10_n0_4 () Bool)
+(declare-fun __ic3_clause_10_n0_5 () Bool)
+(declare-fun __ic3_clause_10_n0_6 () Bool)
+(declare-fun __ic3_clause_10_n0_7 () Bool)
+(declare-fun __ic3_clause_10_n0_8 () Bool)
+(assert (=> _substvar_13444_ _substvar_10018_))
+(assert (=> _substvar_13446_ _substvar_10023_))
+(assert (=> _substvar_13015_ _substvar_13016_))
+(assert (=> _substvar_13449_ _substvar_13450_))
+(assert (=> _substvar_13021_ _substvar_13022_))
+(assert (=> _substvar_13453_ _substvar_13454_))
+(assert (=> _substvar_13027_ _substvar_13456_))
+(assert (=> _substvar_13458_ (= (+ (* (- 1) _substvar_580_) 1) 0)))
+(assert (=> _substvar_13461_ _substvar_13462_))
+(push 1)
+(declare-fun c173 () Bool)
+(declare-fun c181 () Bool)
+(assert _substvar_12544_)
+(assert _substvar_13458_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_30 () Bool)
+(declare-fun __ic3_ind_gen_31 () Bool)
+(declare-fun __ic3_ind_gen_32 () Bool)
+(assert (=> _substvar_13466_ (not (or (not (= (+ (* (- 1) _substvar_856_) 1) 0)) _substvar_21305_ (not (> (* 1 _substvar_857_) 0)) (not _substvar_10044_)))))
+(assert (=> _substvar_13476_ (not (or _substvar_13478_ _substvar_13479_ (not (> (* 1 _substvar_581_) 0)) _substvar_13482_))))
+(assert (=> _substvar_13486_ _substvar_13066_))
+(push 1)
+(declare-fun c183 () Bool)
+(assert _substvar_13476_)
+(check-sat)
+(pop 1)
+(push 1)
+(declare-fun c187 () Bool)
+(declare-fun c188 () Bool)
+(assert _substvar_13466_)
+(assert _substvar_12544_)
+(check-sat)
+(pop 1)
+(declare-fun __ic3_ind_gen_33 () Bool)
+(declare-fun __ic3_ind_gen_34 () Bool)
+(declare-fun __ic3_ind_gen_35 () Bool)
+(assert (=> _substvar_13071_ (not (or _substvar_13072_ (not (> (* 1 _substvar_857_) 0)) (not _substvar_10044_)))))
+(assert (=> _substvar_13079_ (not (or _substvar_13080_ (not (> (* 1 _substvar_581_) 0)) _substvar_13504_))))
+(assert (=> _substvar_13508_ _substvar_12538_))
+(push 1)
+(declare-fun c189 () Bool)
+(assert _substvar_13079_)
+(check-sat)
+(pop 1)
+(declare-fun c193 () Bool)
+(declare-fun c194 () Bool)
+(assert _substvar_13071_)
+(assert _substvar_12544_)
+(check-sat)
+(exit)