From aa0c64d35814ef892dbcd0cec805d44599009c41 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 28 Jun 2018 12:18:47 -0700 Subject: 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. --- src/prop/minisat/core/Solver.cc | 67 +- test/regress/Makefile.tests | 1 + .../DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 | 1182 ++++++++++++++++++++ 3 files changed, 1224 insertions(+), 26 deletions(-) create mode 100644 test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3c8023395..8f5b37e74 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -698,34 +698,49 @@ int Solver::analyze(CRef confl, vec& 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 939b52128..83f1c0714 100644 --- 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 index 000000000..cdaefbfb9 --- /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) -- cgit v1.2.3