From b0f180ff0fccf9bc500501af990c812865d2082b Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 23 Sep 2023 00:18:27 +0400 Subject: [PATCH 1/2] [feat] Separate branch and block coverage --- include/klee/Module/CodeGraphInfo.h | 8 + lib/Core/Executor.cpp | 7 + lib/Core/TargetCalculator.cpp | 163 +- lib/Core/TargetCalculator.h | 9 +- lib/Module/CodeGraphInfo.cpp | 34 + ...r.3.ufo.UNBOUNDED.pals+Problem12_label00.c | 2 +- test/regression/2023-10-16-CostasArray-17.c | 1741 +++++++++++++++++ 7 files changed, 1908 insertions(+), 56 deletions(-) create mode 100644 test/regression/2023-10-16-CostasArray-17.c diff --git a/include/klee/Module/CodeGraphInfo.h b/include/klee/Module/CodeGraphInfo.h index c13a7a03371..f1576336b10 100644 --- a/include/klee/Module/CodeGraphInfo.h +++ b/include/klee/Module/CodeGraphInfo.h @@ -45,6 +45,8 @@ class CodeGraphInfo { functionDistanceList functionSortedBackwardDistance; functionBranchesSet functionBranches; + functionBranchesSet functionConditionalBranches; + functionBranchesSet functionBlocks; private: void calculateDistance(KBlock *bb); @@ -54,6 +56,8 @@ class CodeGraphInfo { void calculateBackwardDistance(KFunction *kf); void calculateFunctionBranches(KFunction *kf); + void calculateFunctionConditionalBranches(KFunction *kf); + void calculateFunctionBlocks(KFunction *kf); public: const std::unordered_map &getDistance(KBlock *kb); @@ -78,6 +82,10 @@ class CodeGraphInfo { const std::map> & getFunctionBranches(KFunction *kf); + const std::map> & + getFunctionConditionalBranches(KFunction *kf); + const std::map> & + getFunctionBlocks(KFunction *kf); }; } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0705439d902..96f55a2b3ac 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -445,6 +445,7 @@ bool allLeafsAreConstant(const ref &expr) { extern llvm::cl::opt MaxConstantAllocationSize; extern llvm::cl::opt MaxSymbolicAllocationSize; extern llvm::cl::opt UseSymbolicSizeAllocation; +extern llvm::cl::opt TrackCoverage; // XXX hack extern "C" unsigned dumpStates, dumpPForest; @@ -4373,6 +4374,7 @@ static std::string terminationTypeFileExtension(StateTerminationType type) { }; void Executor::executeStep(ExecutionState &state) { + KFunction *initKF = state.initPC->parent->parent; if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance && stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) { state.clearCoveredNew(); @@ -4407,6 +4409,11 @@ void Executor::executeStep(ExecutionState &state) { // pressure updateStates(nullptr); } + + if (targetCalculator && TrackCoverage != TrackCoverageBy::None && + targetCalculator->isCovered(initKF)) { + haltExecution = HaltExecution::CovCheck; + } } void Executor::targetedRun(ExecutionState &initialState, KBlock *target, diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index e6a8f8834cb..ecc6d790941 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -35,8 +35,19 @@ llvm::cl::opt TargetCalculatorMode( "Looks for the closest uncovered block by state transitions " "history.")), cl::init(TargetCalculateBy::Default), cl::cat(ExecCat)); + } // namespace klee +llvm::cl::opt TrackCoverage( + "track-coverage", cl::desc("Specifiy the track coverage mode."), + cl::values(clEnumValN(TrackCoverageBy::None, "none", "Not track coverage."), + clEnumValN(TrackCoverageBy::Blocks, "blocks", + "Track only covered block."), + clEnumValN(TrackCoverageBy::Branches, "branches", + "Track only covered conditional branches."), + clEnumValN(TrackCoverageBy::All, "all", "Track all.")), + cl::init(TrackCoverageBy::None), cl::cat(ExecCat)); + void TargetCalculator::update(const ExecutionState &state) { Function *initialFunction = state.getInitPCBlock()->getParent(); @@ -46,28 +57,34 @@ void TargetCalculator::update(const ExecutionState &state) { } if (state.prevPC == state.prevPC->parent->getLastInstruction() && !fullyCoveredFunctions.count(state.prevPC->parent->parent)) { + auto &fBranches = getCoverageTargets(state.prevPC->parent->parent); if (!coveredFunctionsInBranches.count(state.prevPC->parent->parent)) { - unsigned index = 0; - if (!coveredBranches[state.prevPC->parent->parent].count( - state.prevPC->parent)) { - state.coverNew(); - coveredBranches[state.prevPC->parent->parent][state.prevPC->parent]; - } - for (auto succ : successors(state.getPrevPCBlock())) { - if (succ == state.getPCBlock()) { - if (!coveredBranches[state.prevPC->parent->parent] - [state.prevPC->parent] - .count(index)) { - state.coverNew(); - coveredBranches[state.prevPC->parent->parent][state.prevPC->parent] - .insert(index); + if (fBranches.count(state.prevPC->parent) != 0) { + if (!coveredBranches[state.prevPC->parent->parent].count( + state.prevPC->parent)) { + state.coverNew(); + coveredBranches[state.prevPC->parent->parent][state.prevPC->parent]; + } + if (!fBranches.at(state.prevPC->parent).empty()) { + unsigned index = 0; + for (auto succ : successors(state.getPrevPCBlock())) { + if (succ == state.getPCBlock()) { + if (!coveredBranches[state.prevPC->parent->parent] + [state.prevPC->parent] + .count(index)) { + state.coverNew(); + coveredBranches[state.prevPC->parent->parent] + [state.prevPC->parent] + .insert(index); + } + break; + } + ++index; } - break; } - ++index; } - if (codeGraphInfo.getFunctionBranches(state.prevPC->parent->parent) == + if (getCoverageTargets(state.prevPC->parent->parent) == coveredBranches[state.prevPC->parent->parent]) { coveredFunctionsInBranches.insert(state.prevPC->parent->parent); } @@ -88,12 +105,15 @@ void TargetCalculator::update(const ExecutionState &state) { KFunction *calledKFunction = state.prevPC->parent->parent->parent ->functionMap[calledFunction]; if (calledKFunction->numInstructions != 0 && - coveredFunctionsInBranches.count(calledKFunction) == 0) { + coveredFunctionsInBranches.count(calledKFunction) == 0 && + !getCoverageTargets(calledKFunction).empty()) { covered = false; break; } if (!fnsTaken.count(calledKFunction) && - fullyCoveredFunctions.count(calledKFunction) == 0) { + fullyCoveredFunctions.count(calledKFunction) == 0 && + calledKFunction->numInstructions != 0 && + !getCoverageTargets(calledKFunction).empty()) { fns.push_back(calledKFunction); } } @@ -178,6 +198,22 @@ bool TargetCalculator::differenceIsEmpty( return diff.empty(); } +const std::map> & +TargetCalculator::getCoverageTargets(KFunction *kf) { + switch (TrackCoverage) { + case TrackCoverageBy::Blocks: + return codeGraphInfo.getFunctionBlocks(kf); + case TrackCoverageBy::Branches: + return codeGraphInfo.getFunctionConditionalBranches(kf); + case TrackCoverageBy::None: + case TrackCoverageBy::All: + return codeGraphInfo.getFunctionBranches(kf); + + default: + assert(0 && "not implemented"); + } +} + bool TargetCalculator::uncoveredBlockPredicate(ExecutionState *state, KBlock *kblock) { Function *initialFunction = state->getInitPCBlock()->getParent(); @@ -186,20 +222,28 @@ bool TargetCalculator::uncoveredBlockPredicate(ExecutionState *state, std::unordered_map &transitionHistory = transitionsHistory[initialFunction]; bool result = false; - if (coveredBranches[kblock->parent].count(kblock) == 0) { - result = true; - } else { - auto &cb = coveredBranches[kblock->parent][kblock]; - if (isa(kblock) && - cast(kblock)->calledFunctions.size() == 1) { - auto calledFunction = *cast(kblock)->calledFunctions.begin(); - KFunction *calledKFunction = - kblock->parent->parent->functionMap[calledFunction]; - result = fullyCoveredFunctions.count(calledKFunction) == 0 && - calledKFunction->numInstructions; + + auto &fBranches = getCoverageTargets(kblock->parent); + + if (fBranches.count(kblock) != 0 || isa(kblock)) { + if (coveredBranches[kblock->parent].count(kblock) == 0) { + result = true; + } else { + auto &cb = coveredBranches[kblock->parent][kblock]; + if (isa(kblock) && + cast(kblock)->calledFunctions.size() == 1) { + auto calledFunction = + *cast(kblock)->calledFunctions.begin(); + KFunction *calledKFunction = + kblock->parent->parent->functionMap[calledFunction]; + result = fullyCoveredFunctions.count(calledKFunction) == 0 && + calledKFunction->numInstructions; + } + if (fBranches.at(kblock) != cb) { + result |= + kblock->basicBlock->getTerminator()->getNumSuccessors() > cb.size(); + } } - result |= - kblock->basicBlock->getTerminator()->getNumSuccessors() > cb.size(); } switch (TargetCalculatorMode) { @@ -246,29 +290,36 @@ TargetHashSet TargetCalculator::calculate(ExecutionState &state) { if (!blocks.empty()) { TargetHashSet targets; for (auto block : blocks) { - if (coveredBranches[block->parent].count(block) == 0) { - targets.insert(ReachBlockTarget::create(block, false)); - } else { - auto &cb = coveredBranches[block->parent][block]; - bool notCoveredFunction = false; - if (isa(block) && - cast(block)->calledFunctions.size() == 1) { - auto calledFunction = - *cast(block)->calledFunctions.begin(); - KFunction *calledKFunction = - block->parent->parent->functionMap[calledFunction]; - notCoveredFunction = - fullyCoveredFunctions.count(calledKFunction) == 0 && - calledKFunction->numInstructions; - } - if (notCoveredFunction) { - targets.insert(ReachBlockTarget::create(block, true)); + auto &fBranches = getCoverageTargets(block->parent); + + if (fBranches.count(block) != 0 || isa(block)) { + if (coveredBranches[block->parent].count(block) == 0) { + targets.insert(ReachBlockTarget::create(block, false)); } else { - for (unsigned index = 0; - index < block->basicBlock->getTerminator()->getNumSuccessors(); - ++index) { - if (!cb.count(index)) - targets.insert(CoverBranchTarget::create(block, index)); + auto &cb = coveredBranches[block->parent][block]; + bool notCoveredFunction = false; + if (isa(block) && + cast(block)->calledFunctions.size() == 1) { + auto calledFunction = + *cast(block)->calledFunctions.begin(); + KFunction *calledKFunction = + block->parent->parent->functionMap[calledFunction]; + notCoveredFunction = + fullyCoveredFunctions.count(calledKFunction) == 0 && + calledKFunction->numInstructions; + } + if (notCoveredFunction) { + targets.insert(ReachBlockTarget::create(block, true)); + } else { + if (fBranches.at(block) != cb) { + for (unsigned index = 0; + index < + block->basicBlock->getTerminator()->getNumSuccessors(); + ++index) { + if (!cb.count(index)) + targets.insert(CoverBranchTarget::create(block, index)); + } + } } } } @@ -289,3 +340,7 @@ TargetHashSet TargetCalculator::calculate(ExecutionState &state) { return {}; } + +bool TargetCalculator::isCovered(KFunction *kf) const { + return fullyCoveredFunctions.count(kf) != 0; +} diff --git a/lib/Core/TargetCalculator.h b/lib/Core/TargetCalculator.h index 75bd8413d8c..fcf406c0e7b 100644 --- a/lib/Core/TargetCalculator.h +++ b/lib/Core/TargetCalculator.h @@ -36,7 +36,9 @@ class CodeGraphInfo; class ExecutionState; struct TransitionHash; -enum TargetCalculateBy { Default, Blocks, Transitions }; +enum class TargetCalculateBy { Default, Blocks, Transitions }; + +enum class TrackCoverageBy { None, Blocks, Branches, All }; typedef std::pair Transition; typedef std::pair Branch; @@ -77,6 +79,8 @@ class TargetCalculator { TargetHashSet calculate(ExecutionState &state); + bool isCovered(KFunction *kf) const; + private: CodeGraphInfo &codeGraphInfo; BlocksHistory blocksHistory; @@ -96,6 +100,9 @@ class TargetCalculator { const std::unordered_map &history, KBlock *target); + const std::map> & + getCoverageTargets(KFunction *kf); + bool uncoveredBlockPredicate(ExecutionState *state, KBlock *kblock); }; } // namespace klee diff --git a/lib/Module/CodeGraphInfo.cpp b/lib/Module/CodeGraphInfo.cpp index 045c379932d..a0df05e8c12 100644 --- a/lib/Module/CodeGraphInfo.cpp +++ b/lib/Module/CodeGraphInfo.cpp @@ -130,6 +130,26 @@ void CodeGraphInfo::calculateFunctionBranches(KFunction *kf) { } } } +void CodeGraphInfo::calculateFunctionConditionalBranches(KFunction *kf) { + std::map> &fbranches = + functionConditionalBranches[kf]; + for (auto &kb : kf->blocks) { + if (kb->basicBlock->getTerminator()->getNumSuccessors() > 1) { + fbranches[kb.get()]; + for (unsigned branch = 0; + branch < kb->basicBlock->getTerminator()->getNumSuccessors(); + ++branch) { + fbranches[kb.get()].insert(branch); + } + } + } +} +void CodeGraphInfo::calculateFunctionBlocks(KFunction *kf) { + std::map> &fbranches = functionBlocks[kf]; + for (auto &kb : kf->blocks) { + fbranches[kb.get()]; + } +} const std::unordered_map & CodeGraphInfo::getDistance(KBlock *kb) { @@ -219,3 +239,17 @@ CodeGraphInfo::getFunctionBranches(KFunction *kf) { calculateFunctionBranches(kf); return functionBranches.at(kf); } + +const std::map> & +CodeGraphInfo::getFunctionConditionalBranches(KFunction *kf) { + if (functionConditionalBranches.count(kf) == 0) + calculateFunctionConditionalBranches(kf); + return functionConditionalBranches.at(kf); +} + +const std::map> & +CodeGraphInfo::getFunctionBlocks(KFunction *kf) { + if (functionBlocks.count(kf) == 0) + calculateFunctionBlocks(kf); + return functionBlocks.at(kf); +} diff --git a/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c index 36a3bb4ab7c..7b90ea5b2d5 100644 --- a/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c +++ b/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c @@ -1,7 +1,7 @@ // REQUIRES: geq-llvm-14.0 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc +// RUN: %klee --output-dir=%t.klee-out --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc // RUN: %klee-stats --print-columns 'BCov(%)' --table-format=csv %t.klee-out > %t.stats // RUN: FileCheck -input-file=%t.stats %s diff --git a/test/regression/2023-10-16-CostasArray-17.c b/test/regression/2023-10-16-CostasArray-17.c new file mode 100644 index 00000000000..b7285326b4a --- /dev/null +++ b/test/regression/2023-10-16-CostasArray-17.c @@ -0,0 +1,1741 @@ +// RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc +// RUN: %klee-stats --print-columns 'ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats +// RUN: FileCheck -input-file=%t.stats %s + +// Branch coverage 100%, and instruction coverage is very small: +// CHECK: ICov(%),BCov(%) +// CHECK-NEXT: {{(0\.[3-4][0-9])}},100.0 + +#include "klee-test-comp.c" + +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://github.com/sosy-lab/sv-benchmarks +// +// SPDX-FileCopyrightText: 2016 Gilles Audemard +// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community +// +// SPDX-License-Identifier: MIT + +extern void abort(void) __attribute__((__nothrow__, __leaf__)) +__attribute__((__noreturn__)); +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__nothrow__, __leaf__)) +__attribute__((__noreturn__)); +int __VERIFIER_nondet_int(); +void reach_error() { __assert_fail("0", "CostasArray-17.c", 5, "reach_error"); } +void assume(int cond) { + if (!cond) + abort(); +} +int main() { + int cond0; + int dummy = 0; + int N; + int var0; + var0 = __VERIFIER_nondet_int(); + assume(var0 >= 1); + assume(var0 <= 17); + int var1; + var1 = __VERIFIER_nondet_int(); + assume(var1 >= 1); + assume(var1 <= 17); + int var2; + var2 = __VERIFIER_nondet_int(); + assume(var2 >= 1); + assume(var2 <= 17); + int var3; + var3 = __VERIFIER_nondet_int(); + assume(var3 >= 1); + assume(var3 <= 17); + int var4; + var4 = __VERIFIER_nondet_int(); + assume(var4 >= 1); + assume(var4 <= 17); + int var5; + var5 = __VERIFIER_nondet_int(); + assume(var5 >= 1); + assume(var5 <= 17); + int var6; + var6 = __VERIFIER_nondet_int(); + assume(var6 >= 1); + assume(var6 <= 17); + int var7; + var7 = __VERIFIER_nondet_int(); + assume(var7 >= 1); + assume(var7 <= 17); + int var8; + var8 = __VERIFIER_nondet_int(); + assume(var8 >= 1); + assume(var8 <= 17); + int var9; + var9 = __VERIFIER_nondet_int(); + assume(var9 >= 1); + assume(var9 <= 17); + int var10; + var10 = __VERIFIER_nondet_int(); + assume(var10 >= 1); + assume(var10 <= 17); + int var11; + var11 = __VERIFIER_nondet_int(); + assume(var11 >= 1); + assume(var11 <= 17); + int var12; + var12 = __VERIFIER_nondet_int(); + assume(var12 >= 1); + assume(var12 <= 17); + int var13; + var13 = __VERIFIER_nondet_int(); + assume(var13 >= 1); + assume(var13 <= 17); + int var14; + var14 = __VERIFIER_nondet_int(); + assume(var14 >= 1); + assume(var14 <= 17); + int var15; + var15 = __VERIFIER_nondet_int(); + assume(var15 >= 1); + assume(var15 <= 17); + int var16; + var16 = __VERIFIER_nondet_int(); + assume(var16 >= 1); + assume(var16 <= 17); + int var17; + var17 = __VERIFIER_nondet_int(); + assume(var17 >= -16); + assume(var17 <= 16); + assume(var17 != 0); + int var18; + var18 = __VERIFIER_nondet_int(); + assume(var18 >= -16); + assume(var18 <= 16); + assume(var18 != 0); + int var19; + var19 = __VERIFIER_nondet_int(); + assume(var19 >= -16); + assume(var19 <= 16); + assume(var19 != 0); + int var20; + var20 = __VERIFIER_nondet_int(); + assume(var20 >= -16); + assume(var20 <= 16); + assume(var20 != 0); + int var21; + var21 = __VERIFIER_nondet_int(); + assume(var21 >= -16); + assume(var21 <= 16); + assume(var21 != 0); + int var22; + var22 = __VERIFIER_nondet_int(); + assume(var22 >= -16); + assume(var22 <= 16); + assume(var22 != 0); + int var23; + var23 = __VERIFIER_nondet_int(); + assume(var23 >= -16); + assume(var23 <= 16); + assume(var23 != 0); + int var24; + var24 = __VERIFIER_nondet_int(); + assume(var24 >= -16); + assume(var24 <= 16); + assume(var24 != 0); + int var25; + var25 = __VERIFIER_nondet_int(); + assume(var25 >= -16); + assume(var25 <= 16); + assume(var25 != 0); + int var26; + var26 = __VERIFIER_nondet_int(); + assume(var26 >= -16); + assume(var26 <= 16); + assume(var26 != 0); + int var27; + var27 = __VERIFIER_nondet_int(); + assume(var27 >= -16); + assume(var27 <= 16); + assume(var27 != 0); + int var28; + var28 = __VERIFIER_nondet_int(); + assume(var28 >= -16); + assume(var28 <= 16); + assume(var28 != 0); + int var29; + var29 = __VERIFIER_nondet_int(); + assume(var29 >= -16); + assume(var29 <= 16); + assume(var29 != 0); + int var30; + var30 = __VERIFIER_nondet_int(); + assume(var30 >= -16); + assume(var30 <= 16); + assume(var30 != 0); + int var31; + var31 = __VERIFIER_nondet_int(); + assume(var31 >= -16); + assume(var31 <= 16); + assume(var31 != 0); + int var32; + var32 = __VERIFIER_nondet_int(); + assume(var32 >= -16); + assume(var32 <= 16); + assume(var32 != 0); + int var33; + var33 = __VERIFIER_nondet_int(); + assume(var33 >= -16); + assume(var33 <= 16); + assume(var33 != 0); + int var34; + var34 = __VERIFIER_nondet_int(); + assume(var34 >= -16); + assume(var34 <= 16); + assume(var34 != 0); + int var35; + var35 = __VERIFIER_nondet_int(); + assume(var35 >= -16); + assume(var35 <= 16); + assume(var35 != 0); + int var36; + var36 = __VERIFIER_nondet_int(); + assume(var36 >= -16); + assume(var36 <= 16); + assume(var36 != 0); + int var37; + var37 = __VERIFIER_nondet_int(); + assume(var37 >= -16); + assume(var37 <= 16); + assume(var37 != 0); + int var38; + var38 = __VERIFIER_nondet_int(); + assume(var38 >= -16); + assume(var38 <= 16); + assume(var38 != 0); + int var39; + var39 = __VERIFIER_nondet_int(); + assume(var39 >= -16); + assume(var39 <= 16); + assume(var39 != 0); + int var40; + var40 = __VERIFIER_nondet_int(); + assume(var40 >= -16); + assume(var40 <= 16); + assume(var40 != 0); + int var41; + var41 = __VERIFIER_nondet_int(); + assume(var41 >= -16); + assume(var41 <= 16); + assume(var41 != 0); + int var42; + var42 = __VERIFIER_nondet_int(); + assume(var42 >= -16); + assume(var42 <= 16); + assume(var42 != 0); + int var43; + var43 = __VERIFIER_nondet_int(); + assume(var43 >= -16); + assume(var43 <= 16); + assume(var43 != 0); + int var44; + var44 = __VERIFIER_nondet_int(); + assume(var44 >= -16); + assume(var44 <= 16); + assume(var44 != 0); + int var45; + var45 = __VERIFIER_nondet_int(); + assume(var45 >= -16); + assume(var45 <= 16); + assume(var45 != 0); + int var46; + var46 = __VERIFIER_nondet_int(); + assume(var46 >= -16); + assume(var46 <= 16); + assume(var46 != 0); + int var47; + var47 = __VERIFIER_nondet_int(); + assume(var47 >= -16); + assume(var47 <= 16); + assume(var47 != 0); + int var48; + var48 = __VERIFIER_nondet_int(); + assume(var48 >= -16); + assume(var48 <= 16); + assume(var48 != 0); + int var49; + var49 = __VERIFIER_nondet_int(); + assume(var49 >= -16); + assume(var49 <= 16); + assume(var49 != 0); + int var50; + var50 = __VERIFIER_nondet_int(); + assume(var50 >= -16); + assume(var50 <= 16); + assume(var50 != 0); + int var51; + var51 = __VERIFIER_nondet_int(); + assume(var51 >= -16); + assume(var51 <= 16); + assume(var51 != 0); + int var52; + var52 = __VERIFIER_nondet_int(); + assume(var52 >= -16); + assume(var52 <= 16); + assume(var52 != 0); + int var53; + var53 = __VERIFIER_nondet_int(); + assume(var53 >= -16); + assume(var53 <= 16); + assume(var53 != 0); + int var54; + var54 = __VERIFIER_nondet_int(); + assume(var54 >= -16); + assume(var54 <= 16); + assume(var54 != 0); + int var55; + var55 = __VERIFIER_nondet_int(); + assume(var55 >= -16); + assume(var55 <= 16); + assume(var55 != 0); + int var56; + var56 = __VERIFIER_nondet_int(); + assume(var56 >= -16); + assume(var56 <= 16); + assume(var56 != 0); + int var57; + var57 = __VERIFIER_nondet_int(); + assume(var57 >= -16); + assume(var57 <= 16); + assume(var57 != 0); + int var58; + var58 = __VERIFIER_nondet_int(); + assume(var58 >= -16); + assume(var58 <= 16); + assume(var58 != 0); + int var59; + var59 = __VERIFIER_nondet_int(); + assume(var59 >= -16); + assume(var59 <= 16); + assume(var59 != 0); + int var60; + var60 = __VERIFIER_nondet_int(); + assume(var60 >= -16); + assume(var60 <= 16); + assume(var60 != 0); + int var61; + var61 = __VERIFIER_nondet_int(); + assume(var61 >= -16); + assume(var61 <= 16); + assume(var61 != 0); + int var62; + var62 = __VERIFIER_nondet_int(); + assume(var62 >= -16); + assume(var62 <= 16); + assume(var62 != 0); + int var63; + var63 = __VERIFIER_nondet_int(); + assume(var63 >= -16); + assume(var63 <= 16); + assume(var63 != 0); + int var64; + var64 = __VERIFIER_nondet_int(); + assume(var64 >= -16); + assume(var64 <= 16); + assume(var64 != 0); + int var65; + var65 = __VERIFIER_nondet_int(); + assume(var65 >= -16); + assume(var65 <= 16); + assume(var65 != 0); + int var66; + var66 = __VERIFIER_nondet_int(); + assume(var66 >= -16); + assume(var66 <= 16); + assume(var66 != 0); + int var67; + var67 = __VERIFIER_nondet_int(); + assume(var67 >= -16); + assume(var67 <= 16); + assume(var67 != 0); + int var68; + var68 = __VERIFIER_nondet_int(); + assume(var68 >= -16); + assume(var68 <= 16); + assume(var68 != 0); + int var69; + var69 = __VERIFIER_nondet_int(); + assume(var69 >= -16); + assume(var69 <= 16); + assume(var69 != 0); + int var70; + var70 = __VERIFIER_nondet_int(); + assume(var70 >= -16); + assume(var70 <= 16); + assume(var70 != 0); + int var71; + var71 = __VERIFIER_nondet_int(); + assume(var71 >= -16); + assume(var71 <= 16); + assume(var71 != 0); + int var72; + var72 = __VERIFIER_nondet_int(); + assume(var72 >= -16); + assume(var72 <= 16); + assume(var72 != 0); + int var73; + var73 = __VERIFIER_nondet_int(); + assume(var73 >= -16); + assume(var73 <= 16); + assume(var73 != 0); + int var74; + var74 = __VERIFIER_nondet_int(); + assume(var74 >= -16); + assume(var74 <= 16); + assume(var74 != 0); + int var75; + var75 = __VERIFIER_nondet_int(); + assume(var75 >= -16); + assume(var75 <= 16); + assume(var75 != 0); + int var76; + var76 = __VERIFIER_nondet_int(); + assume(var76 >= -16); + assume(var76 <= 16); + assume(var76 != 0); + int var77; + var77 = __VERIFIER_nondet_int(); + assume(var77 >= -16); + assume(var77 <= 16); + assume(var77 != 0); + int var78; + var78 = __VERIFIER_nondet_int(); + assume(var78 >= -16); + assume(var78 <= 16); + assume(var78 != 0); + int var79; + var79 = __VERIFIER_nondet_int(); + assume(var79 >= -16); + assume(var79 <= 16); + assume(var79 != 0); + int var80; + var80 = __VERIFIER_nondet_int(); + assume(var80 >= -16); + assume(var80 <= 16); + assume(var80 != 0); + int var81; + var81 = __VERIFIER_nondet_int(); + assume(var81 >= -16); + assume(var81 <= 16); + assume(var81 != 0); + int var82; + var82 = __VERIFIER_nondet_int(); + assume(var82 >= -16); + assume(var82 <= 16); + assume(var82 != 0); + int var83; + var83 = __VERIFIER_nondet_int(); + assume(var83 >= -16); + assume(var83 <= 16); + assume(var83 != 0); + int var84; + var84 = __VERIFIER_nondet_int(); + assume(var84 >= -16); + assume(var84 <= 16); + assume(var84 != 0); + int var85; + var85 = __VERIFIER_nondet_int(); + assume(var85 >= -16); + assume(var85 <= 16); + assume(var85 != 0); + int var86; + var86 = __VERIFIER_nondet_int(); + assume(var86 >= -16); + assume(var86 <= 16); + assume(var86 != 0); + int var87; + var87 = __VERIFIER_nondet_int(); + assume(var87 >= -16); + assume(var87 <= 16); + assume(var87 != 0); + int var88; + var88 = __VERIFIER_nondet_int(); + assume(var88 >= -16); + assume(var88 <= 16); + assume(var88 != 0); + int var89; + var89 = __VERIFIER_nondet_int(); + assume(var89 >= -16); + assume(var89 <= 16); + assume(var89 != 0); + int var90; + var90 = __VERIFIER_nondet_int(); + assume(var90 >= -16); + assume(var90 <= 16); + assume(var90 != 0); + int var91; + var91 = __VERIFIER_nondet_int(); + assume(var91 >= -16); + assume(var91 <= 16); + assume(var91 != 0); + int var92; + var92 = __VERIFIER_nondet_int(); + assume(var92 >= -16); + assume(var92 <= 16); + assume(var92 != 0); + int var93; + var93 = __VERIFIER_nondet_int(); + assume(var93 >= -16); + assume(var93 <= 16); + assume(var93 != 0); + int var94; + var94 = __VERIFIER_nondet_int(); + assume(var94 >= -16); + assume(var94 <= 16); + assume(var94 != 0); + int var95; + var95 = __VERIFIER_nondet_int(); + assume(var95 >= -16); + assume(var95 <= 16); + assume(var95 != 0); + int var96; + var96 = __VERIFIER_nondet_int(); + assume(var96 >= -16); + assume(var96 <= 16); + assume(var96 != 0); + int var97; + var97 = __VERIFIER_nondet_int(); + assume(var97 >= -16); + assume(var97 <= 16); + assume(var97 != 0); + int var98; + var98 = __VERIFIER_nondet_int(); + assume(var98 >= -16); + assume(var98 <= 16); + assume(var98 != 0); + int var99; + var99 = __VERIFIER_nondet_int(); + assume(var99 >= -16); + assume(var99 <= 16); + assume(var99 != 0); + int var100; + var100 = __VERIFIER_nondet_int(); + assume(var100 >= -16); + assume(var100 <= 16); + assume(var100 != 0); + int var101; + var101 = __VERIFIER_nondet_int(); + assume(var101 >= -16); + assume(var101 <= 16); + assume(var101 != 0); + int var102; + var102 = __VERIFIER_nondet_int(); + assume(var102 >= -16); + assume(var102 <= 16); + assume(var102 != 0); + int var103; + var103 = __VERIFIER_nondet_int(); + assume(var103 >= -16); + assume(var103 <= 16); + assume(var103 != 0); + int var104; + var104 = __VERIFIER_nondet_int(); + assume(var104 >= -16); + assume(var104 <= 16); + assume(var104 != 0); + int var105; + var105 = __VERIFIER_nondet_int(); + assume(var105 >= -16); + assume(var105 <= 16); + assume(var105 != 0); + int var106; + var106 = __VERIFIER_nondet_int(); + assume(var106 >= -16); + assume(var106 <= 16); + assume(var106 != 0); + int var107; + var107 = __VERIFIER_nondet_int(); + assume(var107 >= -16); + assume(var107 <= 16); + assume(var107 != 0); + int var108; + var108 = __VERIFIER_nondet_int(); + assume(var108 >= -16); + assume(var108 <= 16); + assume(var108 != 0); + int var109; + var109 = __VERIFIER_nondet_int(); + assume(var109 >= -16); + assume(var109 <= 16); + assume(var109 != 0); + int var110; + var110 = __VERIFIER_nondet_int(); + assume(var110 >= -16); + assume(var110 <= 16); + assume(var110 != 0); + int var111; + var111 = __VERIFIER_nondet_int(); + assume(var111 >= -16); + assume(var111 <= 16); + assume(var111 != 0); + int var112; + var112 = __VERIFIER_nondet_int(); + assume(var112 >= -16); + assume(var112 <= 16); + assume(var112 != 0); + int var113; + var113 = __VERIFIER_nondet_int(); + assume(var113 >= -16); + assume(var113 <= 16); + assume(var113 != 0); + int var114; + var114 = __VERIFIER_nondet_int(); + assume(var114 >= -16); + assume(var114 <= 16); + assume(var114 != 0); + int var115; + var115 = __VERIFIER_nondet_int(); + assume(var115 >= -16); + assume(var115 <= 16); + assume(var115 != 0); + int var116; + var116 = __VERIFIER_nondet_int(); + assume(var116 >= -16); + assume(var116 <= 16); + assume(var116 != 0); + int var117; + var117 = __VERIFIER_nondet_int(); + assume(var117 >= -16); + assume(var117 <= 16); + assume(var117 != 0); + int var118; + var118 = __VERIFIER_nondet_int(); + assume(var118 >= -16); + assume(var118 <= 16); + assume(var118 != 0); + int var119; + var119 = __VERIFIER_nondet_int(); + assume(var119 >= -16); + assume(var119 <= 16); + assume(var119 != 0); + int var120; + var120 = __VERIFIER_nondet_int(); + assume(var120 >= -16); + assume(var120 <= 16); + assume(var120 != 0); + int var121; + var121 = __VERIFIER_nondet_int(); + assume(var121 >= -16); + assume(var121 <= 16); + assume(var121 != 0); + int var122; + var122 = __VERIFIER_nondet_int(); + assume(var122 >= -16); + assume(var122 <= 16); + assume(var122 != 0); + int var123; + var123 = __VERIFIER_nondet_int(); + assume(var123 >= -16); + assume(var123 <= 16); + assume(var123 != 0); + int var124; + var124 = __VERIFIER_nondet_int(); + assume(var124 >= -16); + assume(var124 <= 16); + assume(var124 != 0); + int var125; + var125 = __VERIFIER_nondet_int(); + assume(var125 >= -16); + assume(var125 <= 16); + assume(var125 != 0); + int var126; + var126 = __VERIFIER_nondet_int(); + assume(var126 >= -16); + assume(var126 <= 16); + assume(var126 != 0); + int var127; + var127 = __VERIFIER_nondet_int(); + assume(var127 >= -16); + assume(var127 <= 16); + assume(var127 != 0); + int var128; + var128 = __VERIFIER_nondet_int(); + assume(var128 >= -16); + assume(var128 <= 16); + assume(var128 != 0); + int var129; + var129 = __VERIFIER_nondet_int(); + assume(var129 >= -16); + assume(var129 <= 16); + assume(var129 != 0); + int var130; + var130 = __VERIFIER_nondet_int(); + assume(var130 >= -16); + assume(var130 <= 16); + assume(var130 != 0); + int var131; + var131 = __VERIFIER_nondet_int(); + assume(var131 >= -16); + assume(var131 <= 16); + assume(var131 != 0); + int var132; + var132 = __VERIFIER_nondet_int(); + assume(var132 >= -16); + assume(var132 <= 16); + assume(var132 != 0); + int var133; + var133 = __VERIFIER_nondet_int(); + assume(var133 >= -16); + assume(var133 <= 16); + assume(var133 != 0); + int var134; + var134 = __VERIFIER_nondet_int(); + assume(var134 >= -16); + assume(var134 <= 16); + assume(var134 != 0); + int var135; + var135 = __VERIFIER_nondet_int(); + assume(var135 >= -16); + assume(var135 <= 16); + assume(var135 != 0); + int var136; + var136 = __VERIFIER_nondet_int(); + assume(var136 >= -16); + assume(var136 <= 16); + assume(var136 != 0); + int var137; + var137 = __VERIFIER_nondet_int(); + assume(var137 >= -16); + assume(var137 <= 16); + assume(var137 != 0); + int var138; + var138 = __VERIFIER_nondet_int(); + assume(var138 >= -16); + assume(var138 <= 16); + assume(var138 != 0); + int var139; + var139 = __VERIFIER_nondet_int(); + assume(var139 >= -16); + assume(var139 <= 16); + assume(var139 != 0); + int var140; + var140 = __VERIFIER_nondet_int(); + assume(var140 >= -16); + assume(var140 <= 16); + assume(var140 != 0); + int var141; + var141 = __VERIFIER_nondet_int(); + assume(var141 >= -16); + assume(var141 <= 16); + assume(var141 != 0); + int var142; + var142 = __VERIFIER_nondet_int(); + assume(var142 >= -16); + assume(var142 <= 16); + assume(var142 != 0); + int var143; + var143 = __VERIFIER_nondet_int(); + assume(var143 >= -16); + assume(var143 <= 16); + assume(var143 != 0); + int var144; + var144 = __VERIFIER_nondet_int(); + assume(var144 >= -16); + assume(var144 <= 16); + assume(var144 != 0); + int var145; + var145 = __VERIFIER_nondet_int(); + assume(var145 >= -16); + assume(var145 <= 16); + assume(var145 != 0); + int var146; + var146 = __VERIFIER_nondet_int(); + assume(var146 >= -16); + assume(var146 <= 16); + assume(var146 != 0); + int var147; + var147 = __VERIFIER_nondet_int(); + assume(var147 >= -16); + assume(var147 <= 16); + assume(var147 != 0); + int var148; + var148 = __VERIFIER_nondet_int(); + assume(var148 >= -16); + assume(var148 <= 16); + assume(var148 != 0); + int var149; + var149 = __VERIFIER_nondet_int(); + assume(var149 >= -16); + assume(var149 <= 16); + assume(var149 != 0); + int myvar0 = 1; + assume(var0 != var1); + assume(var0 != var2); + assume(var0 != var3); + assume(var0 != var4); + assume(var0 != var5); + assume(var0 != var6); + assume(var0 != var7); + assume(var0 != var8); + assume(var0 != var9); + assume(var0 != var10); + assume(var0 != var11); + assume(var0 != var12); + assume(var0 != var13); + assume(var0 != var14); + assume(var0 != var15); + assume(var0 != var16); + assume(var1 != var2); + assume(var1 != var3); + assume(var1 != var4); + assume(var1 != var5); + assume(var1 != var6); + assume(var1 != var7); + assume(var1 != var8); + assume(var1 != var9); + assume(var1 != var10); + assume(var1 != var11); + assume(var1 != var12); + assume(var1 != var13); + assume(var1 != var14); + assume(var1 != var15); + assume(var1 != var16); + assume(var2 != var3); + assume(var2 != var4); + assume(var2 != var5); + assume(var2 != var6); + assume(var2 != var7); + assume(var2 != var8); + assume(var2 != var9); + assume(var2 != var10); + assume(var2 != var11); + assume(var2 != var12); + assume(var2 != var13); + assume(var2 != var14); + assume(var2 != var15); + assume(var2 != var16); + assume(var3 != var4); + assume(var3 != var5); + assume(var3 != var6); + assume(var3 != var7); + assume(var3 != var8); + assume(var3 != var9); + assume(var3 != var10); + assume(var3 != var11); + assume(var3 != var12); + assume(var3 != var13); + assume(var3 != var14); + assume(var3 != var15); + assume(var3 != var16); + assume(var4 != var5); + assume(var4 != var6); + assume(var4 != var7); + assume(var4 != var8); + assume(var4 != var9); + assume(var4 != var10); + assume(var4 != var11); + assume(var4 != var12); + assume(var4 != var13); + assume(var4 != var14); + assume(var4 != var15); + assume(var4 != var16); + assume(var5 != var6); + assume(var5 != var7); + assume(var5 != var8); + assume(var5 != var9); + assume(var5 != var10); + assume(var5 != var11); + assume(var5 != var12); + assume(var5 != var13); + assume(var5 != var14); + assume(var5 != var15); + assume(var5 != var16); + assume(var6 != var7); + assume(var6 != var8); + assume(var6 != var9); + assume(var6 != var10); + assume(var6 != var11); + assume(var6 != var12); + assume(var6 != var13); + assume(var6 != var14); + assume(var6 != var15); + assume(var6 != var16); + assume(var7 != var8); + assume(var7 != var9); + assume(var7 != var10); + assume(var7 != var11); + assume(var7 != var12); + assume(var7 != var13); + assume(var7 != var14); + assume(var7 != var15); + assume(var7 != var16); + assume(var8 != var9); + assume(var8 != var10); + assume(var8 != var11); + assume(var8 != var12); + assume(var8 != var13); + assume(var8 != var14); + assume(var8 != var15); + assume(var8 != var16); + assume(var9 != var10); + assume(var9 != var11); + assume(var9 != var12); + assume(var9 != var13); + assume(var9 != var14); + assume(var9 != var15); + assume(var9 != var16); + assume(var10 != var11); + assume(var10 != var12); + assume(var10 != var13); + assume(var10 != var14); + assume(var10 != var15); + assume(var10 != var16); + assume(var11 != var12); + assume(var11 != var13); + assume(var11 != var14); + assume(var11 != var15); + assume(var11 != var16); + assume(var12 != var13); + assume(var12 != var14); + assume(var12 != var15); + assume(var12 != var16); + assume(var13 != var14); + assume(var13 != var15); + assume(var13 != var16); + assume(var14 != var15); + assume(var14 != var16); + assume(var15 != var16); + assume(var17 != var18); + assume(var17 != var19); + assume(var17 != var20); + assume(var17 != var21); + assume(var17 != var22); + assume(var17 != var23); + assume(var17 != var24); + assume(var17 != var25); + assume(var17 != var26); + assume(var17 != var27); + assume(var17 != var28); + assume(var17 != var29); + assume(var17 != var30); + assume(var17 != var31); + assume(var17 != var32); + assume(var18 != var19); + assume(var18 != var20); + assume(var18 != var21); + assume(var18 != var22); + assume(var18 != var23); + assume(var18 != var24); + assume(var18 != var25); + assume(var18 != var26); + assume(var18 != var27); + assume(var18 != var28); + assume(var18 != var29); + assume(var18 != var30); + assume(var18 != var31); + assume(var18 != var32); + assume(var19 != var20); + assume(var19 != var21); + assume(var19 != var22); + assume(var19 != var23); + assume(var19 != var24); + assume(var19 != var25); + assume(var19 != var26); + assume(var19 != var27); + assume(var19 != var28); + assume(var19 != var29); + assume(var19 != var30); + assume(var19 != var31); + assume(var19 != var32); + assume(var20 != var21); + assume(var20 != var22); + assume(var20 != var23); + assume(var20 != var24); + assume(var20 != var25); + assume(var20 != var26); + assume(var20 != var27); + assume(var20 != var28); + assume(var20 != var29); + assume(var20 != var30); + assume(var20 != var31); + assume(var20 != var32); + assume(var21 != var22); + assume(var21 != var23); + assume(var21 != var24); + assume(var21 != var25); + assume(var21 != var26); + assume(var21 != var27); + assume(var21 != var28); + assume(var21 != var29); + assume(var21 != var30); + assume(var21 != var31); + assume(var21 != var32); + assume(var22 != var23); + assume(var22 != var24); + assume(var22 != var25); + assume(var22 != var26); + assume(var22 != var27); + assume(var22 != var28); + assume(var22 != var29); + assume(var22 != var30); + assume(var22 != var31); + assume(var22 != var32); + assume(var23 != var24); + assume(var23 != var25); + assume(var23 != var26); + assume(var23 != var27); + assume(var23 != var28); + assume(var23 != var29); + assume(var23 != var30); + assume(var23 != var31); + assume(var23 != var32); + assume(var24 != var25); + assume(var24 != var26); + assume(var24 != var27); + assume(var24 != var28); + assume(var24 != var29); + assume(var24 != var30); + assume(var24 != var31); + assume(var24 != var32); + assume(var25 != var26); + assume(var25 != var27); + assume(var25 != var28); + assume(var25 != var29); + assume(var25 != var30); + assume(var25 != var31); + assume(var25 != var32); + assume(var26 != var27); + assume(var26 != var28); + assume(var26 != var29); + assume(var26 != var30); + assume(var26 != var31); + assume(var26 != var32); + assume(var27 != var28); + assume(var27 != var29); + assume(var27 != var30); + assume(var27 != var31); + assume(var27 != var32); + assume(var28 != var29); + assume(var28 != var30); + assume(var28 != var31); + assume(var28 != var32); + assume(var29 != var30); + assume(var29 != var31); + assume(var29 != var32); + assume(var30 != var31); + assume(var30 != var32); + assume(var31 != var32); + assume(var33 != var34); + assume(var33 != var35); + assume(var33 != var36); + assume(var33 != var37); + assume(var33 != var38); + assume(var33 != var39); + assume(var33 != var40); + assume(var33 != var41); + assume(var33 != var42); + assume(var33 != var43); + assume(var33 != var44); + assume(var33 != var45); + assume(var33 != var46); + assume(var33 != var47); + assume(var34 != var35); + assume(var34 != var36); + assume(var34 != var37); + assume(var34 != var38); + assume(var34 != var39); + assume(var34 != var40); + assume(var34 != var41); + assume(var34 != var42); + assume(var34 != var43); + assume(var34 != var44); + assume(var34 != var45); + assume(var34 != var46); + assume(var34 != var47); + assume(var35 != var36); + assume(var35 != var37); + assume(var35 != var38); + assume(var35 != var39); + assume(var35 != var40); + assume(var35 != var41); + assume(var35 != var42); + assume(var35 != var43); + assume(var35 != var44); + assume(var35 != var45); + assume(var35 != var46); + assume(var35 != var47); + assume(var36 != var37); + assume(var36 != var38); + assume(var36 != var39); + assume(var36 != var40); + assume(var36 != var41); + assume(var36 != var42); + assume(var36 != var43); + assume(var36 != var44); + assume(var36 != var45); + assume(var36 != var46); + assume(var36 != var47); + assume(var37 != var38); + assume(var37 != var39); + assume(var37 != var40); + assume(var37 != var41); + assume(var37 != var42); + assume(var37 != var43); + assume(var37 != var44); + assume(var37 != var45); + assume(var37 != var46); + assume(var37 != var47); + assume(var38 != var39); + assume(var38 != var40); + assume(var38 != var41); + assume(var38 != var42); + assume(var38 != var43); + assume(var38 != var44); + assume(var38 != var45); + assume(var38 != var46); + assume(var38 != var47); + assume(var39 != var40); + assume(var39 != var41); + assume(var39 != var42); + assume(var39 != var43); + assume(var39 != var44); + assume(var39 != var45); + assume(var39 != var46); + assume(var39 != var47); + assume(var40 != var41); + assume(var40 != var42); + assume(var40 != var43); + assume(var40 != var44); + assume(var40 != var45); + assume(var40 != var46); + assume(var40 != var47); + assume(var41 != var42); + assume(var41 != var43); + assume(var41 != var44); + assume(var41 != var45); + assume(var41 != var46); + assume(var41 != var47); + assume(var42 != var43); + assume(var42 != var44); + assume(var42 != var45); + assume(var42 != var46); + assume(var42 != var47); + assume(var43 != var44); + assume(var43 != var45); + assume(var43 != var46); + assume(var43 != var47); + assume(var44 != var45); + assume(var44 != var46); + assume(var44 != var47); + assume(var45 != var46); + assume(var45 != var47); + assume(var46 != var47); + assume(var48 != var49); + assume(var48 != var50); + assume(var48 != var51); + assume(var48 != var52); + assume(var48 != var53); + assume(var48 != var54); + assume(var48 != var55); + assume(var48 != var56); + assume(var48 != var57); + assume(var48 != var58); + assume(var48 != var59); + assume(var48 != var60); + assume(var48 != var61); + assume(var49 != var50); + assume(var49 != var51); + assume(var49 != var52); + assume(var49 != var53); + assume(var49 != var54); + assume(var49 != var55); + assume(var49 != var56); + assume(var49 != var57); + assume(var49 != var58); + assume(var49 != var59); + assume(var49 != var60); + assume(var49 != var61); + assume(var50 != var51); + assume(var50 != var52); + assume(var50 != var53); + assume(var50 != var54); + assume(var50 != var55); + assume(var50 != var56); + assume(var50 != var57); + assume(var50 != var58); + assume(var50 != var59); + assume(var50 != var60); + assume(var50 != var61); + assume(var51 != var52); + assume(var51 != var53); + assume(var51 != var54); + assume(var51 != var55); + assume(var51 != var56); + assume(var51 != var57); + assume(var51 != var58); + assume(var51 != var59); + assume(var51 != var60); + assume(var51 != var61); + assume(var52 != var53); + assume(var52 != var54); + assume(var52 != var55); + assume(var52 != var56); + assume(var52 != var57); + assume(var52 != var58); + assume(var52 != var59); + assume(var52 != var60); + assume(var52 != var61); + assume(var53 != var54); + assume(var53 != var55); + assume(var53 != var56); + assume(var53 != var57); + assume(var53 != var58); + assume(var53 != var59); + assume(var53 != var60); + assume(var53 != var61); + assume(var54 != var55); + assume(var54 != var56); + assume(var54 != var57); + assume(var54 != var58); + assume(var54 != var59); + assume(var54 != var60); + assume(var54 != var61); + assume(var55 != var56); + assume(var55 != var57); + assume(var55 != var58); + assume(var55 != var59); + assume(var55 != var60); + assume(var55 != var61); + assume(var56 != var57); + assume(var56 != var58); + assume(var56 != var59); + assume(var56 != var60); + assume(var56 != var61); + assume(var57 != var58); + assume(var57 != var59); + assume(var57 != var60); + assume(var57 != var61); + assume(var58 != var59); + assume(var58 != var60); + assume(var58 != var61); + assume(var59 != var60); + assume(var59 != var61); + assume(var60 != var61); + assume(var62 != var63); + assume(var62 != var64); + assume(var62 != var65); + assume(var62 != var66); + assume(var62 != var67); + assume(var62 != var68); + assume(var62 != var69); + assume(var62 != var70); + assume(var62 != var71); + assume(var62 != var72); + assume(var62 != var73); + assume(var62 != var74); + assume(var63 != var64); + assume(var63 != var65); + assume(var63 != var66); + assume(var63 != var67); + assume(var63 != var68); + assume(var63 != var69); + assume(var63 != var70); + assume(var63 != var71); + assume(var63 != var72); + assume(var63 != var73); + assume(var63 != var74); + assume(var64 != var65); + assume(var64 != var66); + assume(var64 != var67); + assume(var64 != var68); + assume(var64 != var69); + assume(var64 != var70); + assume(var64 != var71); + assume(var64 != var72); + assume(var64 != var73); + assume(var64 != var74); + assume(var65 != var66); + assume(var65 != var67); + assume(var65 != var68); + assume(var65 != var69); + assume(var65 != var70); + assume(var65 != var71); + assume(var65 != var72); + assume(var65 != var73); + assume(var65 != var74); + assume(var66 != var67); + assume(var66 != var68); + assume(var66 != var69); + assume(var66 != var70); + assume(var66 != var71); + assume(var66 != var72); + assume(var66 != var73); + assume(var66 != var74); + assume(var67 != var68); + assume(var67 != var69); + assume(var67 != var70); + assume(var67 != var71); + assume(var67 != var72); + assume(var67 != var73); + assume(var67 != var74); + assume(var68 != var69); + assume(var68 != var70); + assume(var68 != var71); + assume(var68 != var72); + assume(var68 != var73); + assume(var68 != var74); + assume(var69 != var70); + assume(var69 != var71); + assume(var69 != var72); + assume(var69 != var73); + assume(var69 != var74); + assume(var70 != var71); + assume(var70 != var72); + assume(var70 != var73); + assume(var70 != var74); + assume(var71 != var72); + assume(var71 != var73); + assume(var71 != var74); + assume(var72 != var73); + assume(var72 != var74); + assume(var73 != var74); + assume(var75 != var76); + assume(var75 != var77); + assume(var75 != var78); + assume(var75 != var79); + assume(var75 != var80); + assume(var75 != var81); + assume(var75 != var82); + assume(var75 != var83); + assume(var75 != var84); + assume(var75 != var85); + assume(var75 != var86); + assume(var76 != var77); + assume(var76 != var78); + assume(var76 != var79); + assume(var76 != var80); + assume(var76 != var81); + assume(var76 != var82); + assume(var76 != var83); + assume(var76 != var84); + assume(var76 != var85); + assume(var76 != var86); + assume(var77 != var78); + assume(var77 != var79); + assume(var77 != var80); + assume(var77 != var81); + assume(var77 != var82); + assume(var77 != var83); + assume(var77 != var84); + assume(var77 != var85); + assume(var77 != var86); + assume(var78 != var79); + assume(var78 != var80); + assume(var78 != var81); + assume(var78 != var82); + assume(var78 != var83); + assume(var78 != var84); + assume(var78 != var85); + assume(var78 != var86); + assume(var79 != var80); + assume(var79 != var81); + assume(var79 != var82); + assume(var79 != var83); + assume(var79 != var84); + assume(var79 != var85); + assume(var79 != var86); + assume(var80 != var81); + assume(var80 != var82); + assume(var80 != var83); + assume(var80 != var84); + assume(var80 != var85); + assume(var80 != var86); + assume(var81 != var82); + assume(var81 != var83); + assume(var81 != var84); + assume(var81 != var85); + assume(var81 != var86); + assume(var82 != var83); + assume(var82 != var84); + assume(var82 != var85); + assume(var82 != var86); + assume(var83 != var84); + assume(var83 != var85); + assume(var83 != var86); + assume(var84 != var85); + assume(var84 != var86); + assume(var85 != var86); + assume(var87 != var88); + assume(var87 != var89); + assume(var87 != var90); + assume(var87 != var91); + assume(var87 != var92); + assume(var87 != var93); + assume(var87 != var94); + assume(var87 != var95); + assume(var87 != var96); + assume(var87 != var97); + assume(var88 != var89); + assume(var88 != var90); + assume(var88 != var91); + assume(var88 != var92); + assume(var88 != var93); + assume(var88 != var94); + assume(var88 != var95); + assume(var88 != var96); + assume(var88 != var97); + assume(var89 != var90); + assume(var89 != var91); + assume(var89 != var92); + assume(var89 != var93); + assume(var89 != var94); + assume(var89 != var95); + assume(var89 != var96); + assume(var89 != var97); + assume(var90 != var91); + assume(var90 != var92); + assume(var90 != var93); + assume(var90 != var94); + assume(var90 != var95); + assume(var90 != var96); + assume(var90 != var97); + assume(var91 != var92); + assume(var91 != var93); + assume(var91 != var94); + assume(var91 != var95); + assume(var91 != var96); + assume(var91 != var97); + assume(var92 != var93); + assume(var92 != var94); + assume(var92 != var95); + assume(var92 != var96); + assume(var92 != var97); + assume(var93 != var94); + assume(var93 != var95); + assume(var93 != var96); + assume(var93 != var97); + assume(var94 != var95); + assume(var94 != var96); + assume(var94 != var97); + assume(var95 != var96); + assume(var95 != var97); + assume(var96 != var97); + assume(var98 != var99); + assume(var98 != var100); + assume(var98 != var101); + assume(var98 != var102); + assume(var98 != var103); + assume(var98 != var104); + assume(var98 != var105); + assume(var98 != var106); + assume(var98 != var107); + assume(var99 != var100); + assume(var99 != var101); + assume(var99 != var102); + assume(var99 != var103); + assume(var99 != var104); + assume(var99 != var105); + assume(var99 != var106); + assume(var99 != var107); + assume(var100 != var101); + assume(var100 != var102); + assume(var100 != var103); + assume(var100 != var104); + assume(var100 != var105); + assume(var100 != var106); + assume(var100 != var107); + assume(var101 != var102); + assume(var101 != var103); + assume(var101 != var104); + assume(var101 != var105); + assume(var101 != var106); + assume(var101 != var107); + assume(var102 != var103); + assume(var102 != var104); + assume(var102 != var105); + assume(var102 != var106); + assume(var102 != var107); + assume(var103 != var104); + assume(var103 != var105); + assume(var103 != var106); + assume(var103 != var107); + assume(var104 != var105); + assume(var104 != var106); + assume(var104 != var107); + assume(var105 != var106); + assume(var105 != var107); + assume(var106 != var107); + assume(var108 != var109); + assume(var108 != var110); + assume(var108 != var111); + assume(var108 != var112); + assume(var108 != var113); + assume(var108 != var114); + assume(var108 != var115); + assume(var108 != var116); + assume(var109 != var110); + assume(var109 != var111); + assume(var109 != var112); + assume(var109 != var113); + assume(var109 != var114); + assume(var109 != var115); + assume(var109 != var116); + assume(var110 != var111); + assume(var110 != var112); + assume(var110 != var113); + assume(var110 != var114); + assume(var110 != var115); + assume(var110 != var116); + assume(var111 != var112); + assume(var111 != var113); + assume(var111 != var114); + assume(var111 != var115); + assume(var111 != var116); + assume(var112 != var113); + assume(var112 != var114); + assume(var112 != var115); + assume(var112 != var116); + assume(var113 != var114); + assume(var113 != var115); + assume(var113 != var116); + assume(var114 != var115); + assume(var114 != var116); + assume(var115 != var116); + assume(var117 != var118); + assume(var117 != var119); + assume(var117 != var120); + assume(var117 != var121); + assume(var117 != var122); + assume(var117 != var123); + assume(var117 != var124); + assume(var118 != var119); + assume(var118 != var120); + assume(var118 != var121); + assume(var118 != var122); + assume(var118 != var123); + assume(var118 != var124); + assume(var119 != var120); + assume(var119 != var121); + assume(var119 != var122); + assume(var119 != var123); + assume(var119 != var124); + assume(var120 != var121); + assume(var120 != var122); + assume(var120 != var123); + assume(var120 != var124); + assume(var121 != var122); + assume(var121 != var123); + assume(var121 != var124); + assume(var122 != var123); + assume(var122 != var124); + assume(var123 != var124); + assume(var125 != var126); + assume(var125 != var127); + assume(var125 != var128); + assume(var125 != var129); + assume(var125 != var130); + assume(var125 != var131); + assume(var126 != var127); + assume(var126 != var128); + assume(var126 != var129); + assume(var126 != var130); + assume(var126 != var131); + assume(var127 != var128); + assume(var127 != var129); + assume(var127 != var130); + assume(var127 != var131); + assume(var128 != var129); + assume(var128 != var130); + assume(var128 != var131); + assume(var129 != var130); + assume(var129 != var131); + assume(var130 != var131); + assume(var132 != var133); + assume(var132 != var134); + assume(var132 != var135); + assume(var132 != var136); + assume(var132 != var137); + assume(var133 != var134); + assume(var133 != var135); + assume(var133 != var136); + assume(var133 != var137); + assume(var134 != var135); + assume(var134 != var136); + assume(var134 != var137); + assume(var135 != var136); + assume(var135 != var137); + assume(var136 != var137); + assume(var138 != var139); + assume(var138 != var140); + assume(var138 != var141); + assume(var138 != var142); + assume(var139 != var140); + assume(var139 != var141); + assume(var139 != var142); + assume(var140 != var141); + assume(var140 != var142); + assume(var141 != var142); + assume(var143 != var144); + assume(var143 != var145); + assume(var143 != var146); + assume(var144 != var145); + assume(var144 != var146); + assume(var145 != var146); + assume(var147 != var148); + assume(var147 != var149); + assume(var148 != var149); + assume(var0 - var1 == var17); + assume(var1 - var2 == var18); + assume(var2 - var3 == var19); + assume(var3 - var4 == var20); + assume(var4 - var5 == var21); + assume(var5 - var6 == var22); + assume(var6 - var7 == var23); + assume(var7 - var8 == var24); + assume(var8 - var9 == var25); + assume(var9 - var10 == var26); + assume(var10 - var11 == var27); + assume(var11 - var12 == var28); + assume(var12 - var13 == var29); + assume(var13 - var14 == var30); + assume(var14 - var15 == var31); + assume(var15 - var16 == var32); + assume(var0 - var2 == var33); + assume(var1 - var3 == var34); + assume(var2 - var4 == var35); + assume(var3 - var5 == var36); + assume(var4 - var6 == var37); + assume(var5 - var7 == var38); + assume(var6 - var8 == var39); + assume(var7 - var9 == var40); + assume(var8 - var10 == var41); + assume(var9 - var11 == var42); + assume(var10 - var12 == var43); + assume(var11 - var13 == var44); + assume(var12 - var14 == var45); + assume(var13 - var15 == var46); + assume(var14 - var16 == var47); + assume(var0 - var3 == var48); + assume(var1 - var4 == var49); + assume(var2 - var5 == var50); + assume(var3 - var6 == var51); + assume(var4 - var7 == var52); + assume(var5 - var8 == var53); + assume(var6 - var9 == var54); + assume(var7 - var10 == var55); + assume(var8 - var11 == var56); + assume(var9 - var12 == var57); + assume(var10 - var13 == var58); + assume(var11 - var14 == var59); + assume(var12 - var15 == var60); + assume(var13 - var16 == var61); + assume(var0 - var4 == var62); + assume(var1 - var5 == var63); + assume(var2 - var6 == var64); + assume(var3 - var7 == var65); + assume(var4 - var8 == var66); + assume(var5 - var9 == var67); + assume(var6 - var10 == var68); + assume(var7 - var11 == var69); + assume(var8 - var12 == var70); + assume(var9 - var13 == var71); + assume(var10 - var14 == var72); + assume(var11 - var15 == var73); + assume(var12 - var16 == var74); + assume(var0 - var5 == var75); + assume(var1 - var6 == var76); + assume(var2 - var7 == var77); + assume(var3 - var8 == var78); + assume(var4 - var9 == var79); + assume(var5 - var10 == var80); + assume(var6 - var11 == var81); + assume(var7 - var12 == var82); + assume(var8 - var13 == var83); + assume(var9 - var14 == var84); + assume(var10 - var15 == var85); + assume(var11 - var16 == var86); + assume(var0 - var6 == var87); + assume(var1 - var7 == var88); + assume(var2 - var8 == var89); + assume(var3 - var9 == var90); + assume(var4 - var10 == var91); + assume(var5 - var11 == var92); + assume(var6 - var12 == var93); + assume(var7 - var13 == var94); + assume(var8 - var14 == var95); + assume(var9 - var15 == var96); + assume(var10 - var16 == var97); + assume(var0 - var7 == var98); + assume(var1 - var8 == var99); + assume(var2 - var9 == var100); + assume(var3 - var10 == var101); + assume(var4 - var11 == var102); + assume(var5 - var12 == var103); + assume(var6 - var13 == var104); + assume(var7 - var14 == var105); + assume(var8 - var15 == var106); + assume(var9 - var16 == var107); + assume(var0 - var8 == var108); + assume(var1 - var9 == var109); + assume(var2 - var10 == var110); + assume(var3 - var11 == var111); + assume(var4 - var12 == var112); + assume(var5 - var13 == var113); + assume(var6 - var14 == var114); + assume(var7 - var15 == var115); + assume(var8 - var16 == var116); + assume(var0 - var9 == var117); + assume(var1 - var10 == var118); + assume(var2 - var11 == var119); + assume(var3 - var12 == var120); + assume(var4 - var13 == var121); + assume(var5 - var14 == var122); + assume(var6 - var15 == var123); + assume(var7 - var16 == var124); + assume(var0 - var10 == var125); + assume(var1 - var11 == var126); + assume(var2 - var12 == var127); + assume(var3 - var13 == var128); + assume(var4 - var14 == var129); + assume(var5 - var15 == var130); + assume(var6 - var16 == var131); + assume(var0 - var11 == var132); + assume(var1 - var12 == var133); + assume(var2 - var13 == var134); + assume(var3 - var14 == var135); + assume(var4 - var15 == var136); + assume(var5 - var16 == var137); + assume(var0 - var12 == var138); + assume(var1 - var13 == var139); + assume(var2 - var14 == var140); + assume(var3 - var15 == var141); + assume(var4 - var16 == var142); + assume(var0 - var13 == var143); + assume(var1 - var14 == var144); + assume(var2 - var15 == var145); + assume(var3 - var16 == var146); + assume(var0 - var14 == var147); + assume(var1 - var15 == var148); + assume(var2 - var16 == var149); + assume((var0 - var15) != (var1 - var16)); + reach_error(); + return 0; /* 0 x[0]1 x[1]2 x[2]3 x[3]4 x[4]5 x[5]6 x[6]7 x[7]8 x[8]9 x[9]10 + x[10]11 x[11]12 x[12]13 x[13]14 x[14]15 x[15]16 x[16]17 y[0]18 + y[1]19 y[2]20 y[3]21 y[4]22 y[5]23 y[6]24 y[7]25 y[8]26 y[9]27 + y[10]28 y[11]29 y[12]30 y[13]31 y[14]32 y[15]33 y[16]34 y[17]35 + y[18]36 y[19]37 y[20]38 y[21]39 y[22]40 y[23]41 y[24]42 y[25]43 + y[26]44 y[27]45 y[28]46 y[29]47 y[30]48 y[31]49 y[32]50 y[33]51 + y[34]52 y[35]53 y[36]54 y[37]55 y[38]56 y[39]57 y[40]58 y[41]59 + y[42]60 y[43]61 y[44]62 y[45]63 y[46]64 y[47]65 y[48]66 y[49]67 + y[50]68 y[51]69 y[52]70 y[53]71 y[54]72 y[55]73 y[56]74 y[57]75 + y[58]76 y[59]77 y[60]78 y[61]79 y[62]80 y[63]81 y[64]82 y[65]83 + y[66]84 y[67]85 y[68]86 y[69]87 y[70]88 y[71]89 y[72]90 y[73]91 + y[74]92 y[75]93 y[76]94 y[77]95 y[78]96 y[79]97 y[80]98 y[81]99 + y[82]100 y[83]101 y[84]102 y[85]103 y[86]104 y[87]105 y[88]106 + y[89]107 y[90]108 y[91]109 y[92]110 y[93]111 y[94]112 y[95]113 + y[96]114 y[97]115 y[98]116 y[99]117 y[100]118 y[101]119 y[102]120 + y[103]121 y[104]122 y[105]123 y[106]124 y[107]125 y[108]126 + y[109]127 y[110]128 y[111]129 y[112]130 y[113]131 y[114]132 + y[115]133 y[116]134 y[117]135 y[118]136 y[119]137 y[120]138 + y[121]139 y[122]140 y[123]141 y[124]142 y[125]143 y[126]144 + y[127]145 y[128]146 y[129]147 y[130]148 y[131]149 y[132] */ +} \ No newline at end of file From 54f6c5a86f8824cdf2efce85f6db650ff172ca1e Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 16 Oct 2023 12:49:15 +0400 Subject: [PATCH 2/2] [chore] Update build.sh --- build.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/build.sh b/build.sh index 7d575dad089..cc41037dcbf 100755 --- a/build.sh +++ b/build.sh @@ -29,9 +29,9 @@ SQLITE_VERSION="3400100" ## LLVM Required options LLVM_VERSION=14 ENABLE_OPTIMIZED=1 -ENABLE_DEBUG=1 +ENABLE_DEBUG=0 DISABLE_ASSERTIONS=1 -REQUIRES_RTTI=1 +REQUIRES_RTTI=0 ## Solvers Required options # SOLVERS=STP