./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-145.smt2 .


--------------------------------------------------------------------------------


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:47,255 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:47,374 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3d214016-6b9b-46cc-ae71-61f3fc62cd73/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:47,380 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:47,383 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:47,420 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:47,421 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:47,421 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:47,423 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:47,423 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:47,424 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:47,425 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:47,426 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:47,426 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:47,426 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:47,426 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:47,427 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:47,427 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:47,427 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:47,428 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:47,428 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:47,428 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:47,428 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:47,428 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:47,428 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:47,429 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:47,429 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:47,784 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:47,794 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:47,796 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:47,798 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:47,798 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:47,800 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3d214016-6b9b-46cc-ae71-61f3fc62cd73/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-145.smt2
[2025-04-28 21:21:47,801 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:47,806 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:49,164 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3d214016-6b9b-46cc-ae71-61f3fc62cd73/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-145.smt2
[2025-04-28 21:21:49,168 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:49,171 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:49,172 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:49,172 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:49,172 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:49,175 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,318 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49 Unit
[2025-04-28 21:21:49,319 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:49,321 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:49,321 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:49,321 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:49,339 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,340 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,405 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,406 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,456 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,462 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,464 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,472 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,477 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,531 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:49,532 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:49,532 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:49,532 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:49,533 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,536 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:49,552 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,566 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,571 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,583 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:49,583 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:49,583 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:49,583 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATldv_blast_assert.split given in one single declaration
[2025-04-28 21:21:49,584 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATldv_blast_assert.split
[2025-04-28 21:21:49,584 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATldv_blast_assert.split
[2025-04-28 21:21:49,584 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:49,584 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:49,584 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:49,584 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATNodeBlock.i.us given in one single declaration
[2025-04-28 21:21:49,584 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATNodeBlock.i.us
[2025-04-28 21:21:49,585 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATNodeBlock.i.us
[2025-04-28 21:21:49,585 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATNodeBlock.i.lr.ph given in one single declaration
[2025-04-28 21:21:49,585 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATNodeBlock.i.lr.ph
[2025-04-28 21:21:49,585 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATNodeBlock.i.lr.ph
[2025-04-28 21:21:49,585 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATNodeBlock.i.us45 given in one single declaration
[2025-04-28 21:21:49,585 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATNodeBlock.i.us45
[2025-04-28 21:21:49,586 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATNodeBlock.i.us45
[2025-04-28 21:21:49,586 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATNodeBlock.i.us.us given in one single declaration
[2025-04-28 21:21:49,587 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATNodeBlock.i.us.us
[2025-04-28 21:21:49,587 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATNodeBlock.i.us.us
[2025-04-28 21:21:49,587 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:49,587 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:49,587 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:50,004 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:50,008 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:52,062 INFO  L?                        ?]: Removed 1797 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:52,063 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:52,080 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:52,081 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:52,082 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:52 BoogieIcfgContainer
[2025-04-28 21:21:52,082 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:52,084 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:52,085 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:52,089 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:52,090 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:49" (1/3) ...
[2025-04-28 21:21:52,091 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3f4056a2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:52, skipping insertion in model container
[2025-04-28 21:21:52,091 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (2/3) ...
[2025-04-28 21:21:52,091 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3f4056a2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:52, skipping insertion in model container
[2025-04-28 21:21:52,092 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:52" (3/3) ...
[2025-04-28 21:21:52,093 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:52,110 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:52,113 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 36 locations, 61 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:52,176 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:52,198 INFO  L340      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=None, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@1614a901, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:52,198 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:52,202 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 36 states, 15 states have (on average 1.4666666666666666) internal successors, (22), 22 states have internal predecessors, (22), 13 states have call successors, (13), 7 states have call predecessors, (13), 7 states have return successors, (13), 7 states have call predecessors, (13), 13 states have call successors, (13)
[2025-04-28 21:21:52,211 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:52,211 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,212 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:52,212 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,218 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,219 INFO  L85        PathProgramCache]: Analyzing trace with hash 103131279, now seen corresponding path program 1 times
[2025-04-28 21:21:52,228 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,228 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [213880740]
[2025-04-28 21:21:52,228 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,229 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,263 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:52,266 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:52,266 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,266 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,300 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:52,301 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,302 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [213880740]
[2025-04-28 21:21:52,305 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [213880740] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,305 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,310 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:52,312 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1566876893]
[2025-04-28 21:21:52,313 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,320 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:52,321 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,355 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:52,356 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:52,358 INFO  L87              Difference]: Start difference. First operand  has 36 states, 15 states have (on average 1.4666666666666666) internal successors, (22), 22 states have internal predecessors, (22), 13 states have call successors, (13), 7 states have call predecessors, (13), 7 states have return successors, (13), 7 states have call predecessors, (13), 13 states have call successors, (13) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:52,387 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,387 INFO  L93              Difference]: Finished difference Result 33 states and 42 transitions.
[2025-04-28 21:21:52,388 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:52,390 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-04-28 21:21:52,390 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,398 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:52,398 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:52,402 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:52,405 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 42 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,411 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 42 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:52,430 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:52,452 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:52,453 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 13 states have (on average 1.3846153846153846) internal successors, (18), 18 states have internal predecessors, (18), 12 states have call successors, (12), 7 states have call predecessors, (12), 7 states have return successors, (12), 7 states have call predecessors, (12), 12 states have call successors, (12)
[2025-04-28 21:21:52,461 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 42 transitions.
[2025-04-28 21:21:52,463 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 42 transitions. Word has length 5
[2025-04-28 21:21:52,463 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,463 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 42 transitions.
[2025-04-28 21:21:52,464 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:52,464 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 42 transitions.
[2025-04-28 21:21:52,465 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:52,467 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,467 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,467 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:52,468 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,468 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,468 INFO  L85        PathProgramCache]: Analyzing trace with hash -240654111, now seen corresponding path program 1 times
[2025-04-28 21:21:52,469 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,469 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [818243940]
[2025-04-28 21:21:52,469 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,469 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,504 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:52,623 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:52,623 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,623 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,205 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:53,206 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,206 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [818243940]
[2025-04-28 21:21:53,206 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [818243940] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,206 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,206 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:53,206 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1161258085]
[2025-04-28 21:21:53,206 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,208 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:53,208 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,210 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:53,210 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:53,210 INFO  L87              Difference]: Start difference. First operand 33 states and 42 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:53,568 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,569 INFO  L93              Difference]: Finished difference Result 35 states and 45 transitions.
[2025-04-28 21:21:53,571 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:53,571 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 19
[2025-04-28 21:21:53,572 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,574 INFO  L225             Difference]: With dead ends: 35
[2025-04-28 21:21:53,574 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:21:53,575 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:53,576 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 1 mSDsluCounter, 68 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 108 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,576 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 108 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:53,578 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:21:53,588 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 35.
[2025-04-28 21:21:53,590 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 14 states have (on average 1.3571428571428572) internal successors, (19), 19 states have internal predecessors, (19), 12 states have call successors, (12), 7 states have call predecessors, (12), 8 states have return successors, (14), 8 states have call predecessors, (14), 12 states have call successors, (14)
[2025-04-28 21:21:53,591 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 45 transitions.
[2025-04-28 21:21:53,591 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 45 transitions. Word has length 19
[2025-04-28 21:21:53,593 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,593 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 45 transitions.
[2025-04-28 21:21:53,593 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:53,593 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 45 transitions.
[2025-04-28 21:21:53,594 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:53,595 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,596 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,596 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:53,596 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,597 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,598 INFO  L85        PathProgramCache]: Analyzing trace with hash 197381728, now seen corresponding path program 1 times
[2025-04-28 21:21:53,598 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,598 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [264709911]
[2025-04-28 21:21:53,598 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,598 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,786 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:55,087 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:55,087 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,087 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:55,088 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-04-28 21:21:55,120 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:55,723 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:55,724 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,724 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:55,792 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-04-28 21:21:55,793 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-04-28 21:21:55,794 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:55,796 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:55,801 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1]
[2025-04-28 21:21:55,826 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:55,830 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:55 BoogieIcfgContainer
[2025-04-28 21:21:55,830 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:55,831 INFO  L158              Benchmark]: Toolchain (without parser) took 6660.57ms. Allocated memory is still 234.9MB. Free memory was 181.6MB in the beginning and 78.8MB in the end (delta: 102.9MB). Peak memory consumption was 122.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:55,831 INFO  L158              Benchmark]: SmtParser took 0.40ms. Allocated memory is still 234.9MB. Free memory is still 171.2MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:55,832 INFO  L158              Benchmark]: ChcToBoogie took 147.93ms. Allocated memory is still 234.9MB. Free memory was 181.6MB in the beginning and 164.9MB in the end (delta: 16.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:55,832 INFO  L158              Benchmark]: Boogie Preprocessor took 209.96ms. Allocated memory is still 234.9MB. Free memory was 164.9MB in the beginning and 159.8MB in the end (delta: 5.2MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:55,832 INFO  L158              Benchmark]: RCFGBuilder took 2550.34ms. Allocated memory is still 234.9MB. Free memory was 159.8MB in the beginning and 113.6MB in the end (delta: 46.1MB). Peak memory consumption was 93.0MB. Max. memory is 33.6GB.
[2025-04-28 21:21:55,833 INFO  L158              Benchmark]: TraceAbstraction took 3746.37ms. Allocated memory is still 234.9MB. Free memory was 113.6MB in the beginning and 78.8MB in the end (delta: 34.9MB). Peak memory consumption was 47.9MB. Max. memory is 33.6GB.
[2025-04-28 21:21:55,836 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.40ms. Allocated memory is still 234.9MB. Free memory is still 171.2MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 147.93ms. Allocated memory is still 234.9MB. Free memory was 181.6MB in the beginning and 164.9MB in the end (delta: 16.7MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 209.96ms. Allocated memory is still 234.9MB. Free memory was 164.9MB in the beginning and 159.8MB in the end (delta: 5.2MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * RCFGBuilder took 2550.34ms. Allocated memory is still 234.9MB. Free memory was 159.8MB in the beginning and 113.6MB in the end (delta: 46.1MB). Peak memory consumption was 93.0MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3746.37ms. Allocated memory is still 234.9MB. Free memory was 113.6MB in the beginning and 78.8MB in the end (delta: 34.9MB). Peak memory consumption was 47.9MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - CounterExampleResult [Unknown line] : the set of constraint Horn clauses is unsatisfiable
    the set of constraint Horn clauses is unsatisfiable
We found a FailurePath: 
[L0]  CALL  call False();
[L0]  CALL  call main.ATldv_blast_assert.split();
[L0]        assume ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((!((hbv_main.ATldv_blast_assert.split_U4_127 <= 0 && hbv_main.ATldv_blast_assert.split_F5_77) && 0 < hbv_main.ATldv_blast_assert.split_L5_76) && !(hbv_main.ATldv_blast_assert.split_Q6_483 <= 0 && hbv_main.ATldv_blast_assert.split_P6_153)) && !((0 < hbv_main.ATldv_blast_assert.split_Q5_326 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_S5_327 <= 0)) && !(hbv_main.ATldv_blast_assert.split_K2_318[hbv_main.ATldv_blast_assert.split_L2_236 := hbv_main.ATldv_blast_assert.split_M2_377] != hbv_main.ATldv_blast_assert.split_N2_378 && hbv_main.ATldv_blast_assert.split_I4_52)) && !(!hbv_main.ATldv_blast_assert.split_A14_295 && hbv_main.ATldv_blast_assert.split_B14_294)) && !(hbv_main.ATldv_blast_assert.split_S_5 && hbv_main.ATldv_blast_assert.split_J17_4[hbv_main.ATldv_blast_assert.split_V15_188] != hbv_main.ATldv_blast_assert.split_W15_501)) && hbv_main.ATldv_blast_assert.split_R1_92 == hbv_main.ATldv_blast_assert.split_C_56) && hbv_main.ATldv_blast_assert.split_N3_174 == 6 + hbv_main.ATldv_blast_assert.split_M3_175) && hbv_main.ATldv_blast_assert.split_G17_374 == hbv_main.ATldv_blast_assert.split_S17_441) && !((hbv_main.ATldv_blast_assert.split_L15_323 && hbv_main.ATldv_blast_assert.split_S_5) && hbv_main.ATldv_blast_assert.split_J17_4 != hbv_main.ATldv_blast_assert.split_J15_148)) && hbv_main.ATldv_blast_assert.split_G11_93 == hbv_main.ATldv_blast_assert.split_E11_94) && 160 + hbv_main.ATldv_blast_assert.split_B13_12 == hbv_main.ATldv_blast_assert.split_D13_200) && hbv_main.ATldv_blast_assert.split_C_56 + 26 == hbv_main.ATldv_blast_assert.split_B2_122) && !((hbv_main.ATldv_blast_assert.split_O1_44 && 0 < hbv_main.ATldv_blast_assert.split_K16_46) && hbv_main.ATldv_blast_assert.split_W8_107 <= 0)) && hbv_main.ATldv_blast_assert.split_F15_100 == hbv_main.ATldv_blast_assert.split_V13_514) && hbv_main.ATldv_blast_assert.split_V8_286 == hbv_main.ATldv_blast_assert.split_T8_45) && !(hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_J6_305)) && !((0 < hbv_main.ATldv_blast_assert.split_C3_172 && hbv_main.ATldv_blast_assert.split_D3_173 <= 0) && hbv_main.ATldv_blast_assert.split_I4_52)) && !((hbv_main.ATldv_blast_assert.split_R7_23 && hbv_main.ATldv_blast_assert.split_A7_53) && !hbv_main.ATldv_blast_assert.split_B7_54)) && !(hbv_main.ATldv_blast_assert.split_P10_434 <= 0 && hbv_main.ATldv_blast_assert.split_J8_273)) && hbv_main.ATldv_blast_assert.split_I2_287 == hbv_main.ATldv_blast_assert.split_J2_468) && hbv_main.ATldv_blast_assert.split_O10_68 + 24 == hbv_main.ATldv_blast_assert.split_H9_42) && !(hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_A6_358)) && hbv_main.ATldv_blast_assert.split_O17_130 == hbv_main.ATldv_blast_assert.split_W17_353) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_G9_41 != hbv_main.ATldv_blast_assert.split_D9_386[hbv_main.ATldv_blast_assert.split_E9_283 := hbv_main.ATldv_blast_assert.split_F9_456])) && !((!hbv_main.ATldv_blast_assert.split_W4_411 && hbv_main.ATldv_blast_assert.split_V4_207) && hbv_main.ATldv_blast_assert.split_J5_224)) && hbv_main.ATldv_blast_assert.split_Y4_66 == hbv_main.ATldv_blast_assert.split_O3_321) && 184 + hbv_main.ATldv_blast_assert.split_B13_12 == hbv_main.ATldv_blast_assert.split_R11_62) && !((hbv_main.ATldv_blast_assert.split_R16_205 != hbv_main.ATldv_blast_assert.split_M14_473 && hbv_main.ATldv_blast_assert.split_O14_170) && hbv_main.ATldv_blast_assert.split_W16_136)) && !((!hbv_main.ATldv_blast_assert.split_P16_350 && hbv_main.ATldv_blast_assert.split_W16_136) && hbv_main.ATldv_blast_assert.split_X16_135)) && hbv_main.ATldv_blast_assert.split_J10_333 == 40 + hbv_main.ATldv_blast_assert.split_O10_68) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_G9_41[hbv_main.ATldv_blast_assert.split_H9_42 := 3] != hbv_main.ATldv_blast_assert.split_K9_43)) && !(hbv_main.ATldv_blast_assert.split_R9_370 != hbv_main.ATldv_blast_assert.split_P9_369[hbv_main.ATldv_blast_assert.split_O9_516] && hbv_main.ATldv_blast_assert.split_O1_44)) && !((!hbv_main.ATldv_blast_assert.split_R6_152 || !hbv_main.ATldv_blast_assert.split_T6_89) && hbv_main.ATldv_blast_assert.split_R6_152)) && !((hbv_main.ATldv_blast_assert.split_E6_298 != hbv_main.ATldv_blast_assert.split_B19_299 && hbv_main.ATldv_blast_assert.split_L19_109) && hbv_main.ATldv_blast_assert.split_L6_106)) && !((hbv_main.ATldv_blast_assert.split_L15_323 && hbv_main.ATldv_blast_assert.split_S_5) && hbv_main.ATldv_blast_assert.split_M15_8 != hbv_main.ATldv_blast_assert.split_V15_188)) && !((!hbv_main.ATldv_blast_assert.split_X14_145 || !hbv_main.ATldv_blast_assert.split_C1_6) && hbv_main.ATldv_blast_assert.split_C1_6)) && !((hbv_main.ATldv_blast_assert.split_N15_189 != hbv_main.ATldv_blast_assert.split_J17_4 && hbv_main.ATldv_blast_assert.split_P15_113) && hbv_main.ATldv_blast_assert.split_S_5)) && !((hbv_main.ATldv_blast_assert.split_J1_494 != 0 || !hbv_main.ATldv_blast_assert.split_B7_54) && (hbv_main.ATldv_blast_assert.split_B7_54 || hbv_main.ATldv_blast_assert.split_J1_494 == 0))) && !((hbv_main.ATldv_blast_assert.split_R7_23 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_X7_234 != hbv_main.ATldv_blast_assert.split_S7_131)) && !((hbv_main.ATldv_blast_assert.split_F12_79 && hbv_main.ATldv_blast_assert.split_D12_487) && hbv_main.ATldv_blast_assert.split_C12_432)) && hbv_main.ATldv_blast_assert.split_L1_18 == hbv_main.ATldv_blast_assert.split_O10_68 + 80) && !(hbv_main.ATldv_blast_assert.split_B1_308 && !hbv_main.ATldv_blast_assert.split_A1_274)) && hbv_main.ATldv_blast_assert.split_F15_100 == hbv_main.ATldv_blast_assert.split_P8_433) && !((hbv_main.ATldv_blast_assert.split_A13_125 != hbv_main.ATldv_blast_assert.split_C13_199 && hbv_main.ATldv_blast_assert.split_J1_27) && hbv_main.ATldv_blast_assert.split_M1_17)) && hbv_main.ATldv_blast_assert.split_S16_169 == hbv_main.ATldv_blast_assert.split_Y16_455) && !((hbv_main.ATldv_blast_assert.split_U14_437 || hbv_main.ATldv_blast_assert.split_S8_438 == 0) && (hbv_main.ATldv_blast_assert.split_S8_438 != 0 || !hbv_main.ATldv_blast_assert.split_U14_437))) && !((hbv_main.ATldv_blast_assert.split_N16_500 != hbv_main.ATldv_blast_assert.split_M16_187 && hbv_main.ATldv_blast_assert.split_L16_197) && hbv_main.ATldv_blast_assert.split_H18_31)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_T2_401 != hbv_main.ATldv_blast_assert.split_V2_400[hbv_main.ATldv_blast_assert.split_W2_227])) && hbv_main.ATldv_blast_assert.split_I7_158 == hbv_main.ATldv_blast_assert.split_G1_73) && hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_Y14_144) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_O11_60 != hbv_main.ATldv_blast_assert.split_L11_57[hbv_main.ATldv_blast_assert.split_E_58 := hbv_main.ATldv_blast_assert.split_N11_59])) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_E3_264 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_M3_175)) && hbv_main.ATldv_blast_assert.split_H11_116 == hbv_main.ATldv_blast_assert.split_O_272) && !((hbv_main.ATldv_blast_assert.split_V9_157 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && !((hbv_main.ATldv_blast_assert.split_T4_213 && (!hbv_main.ATldv_blast_assert.split_V4_207 || !hbv_main.ATldv_blast_assert.split_S4_212)) && (!hbv_main.ATldv_blast_assert.split_Q4_214 || !hbv_main.ATldv_blast_assert.split_P4_91))) && !((!hbv_main.ATldv_blast_assert.split_P6_153 && hbv_main.ATldv_blast_assert.split_T6_89) && hbv_main.ATldv_blast_assert.split_U6_88)) && !((hbv_main.ATldv_blast_assert.split_D16_167 && hbv_main.ATldv_blast_assert.split_C16_168) && !hbv_main.ATldv_blast_assert.split_Y15_399)) && hbv_main.ATldv_blast_assert.split_E2_39 == hbv_main.ATldv_blast_assert.split_O_40) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_Y1_176 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_G4_177)) && !((hbv_main.ATldv_blast_assert.split_N19_220 != hbv_main.ATldv_blast_assert.split_V19_163 && hbv_main.ATldv_blast_assert.split_P19_34) && hbv_main.ATldv_blast_assert.split_D20_35)) && !(hbv_main.ATldv_blast_assert.split_Y6_102 && (!hbv_main.ATldv_blast_assert.split_L6_106 || !hbv_main.ATldv_blast_assert.split_Y6_102))) && !((0 < hbv_main.ATldv_blast_assert.split_D7_142 && hbv_main.ATldv_blast_assert.split_R7_23) && hbv_main.ATldv_blast_assert.split_C7_459 <= 0)) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_Z17_72) && hbv_main.ATldv_blast_assert.split_J18_69 != hbv_main.ATldv_blast_assert.split_X17_70)) && !(hbv_main.ATldv_blast_assert.split_D7_142 <= 0 && hbv_main.ATldv_blast_assert.split_L6_106)) && !((hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_M6_492)) && !(0 < hbv_main.ATldv_blast_assert.split_Z15_301 && !hbv_main.ATldv_blast_assert.split_Y15_399)) && !((hbv_main.ATldv_blast_assert.split_O14_170 && hbv_main.ATldv_blast_assert.split_W16_136) && hbv_main.ATldv_blast_assert.split_R14_398 != hbv_main.ATldv_blast_assert.split_P14_269)) && !((!hbv_main.ATldv_blast_assert.split_C8_239 || !hbv_main.ATldv_blast_assert.split_P19_34) && hbv_main.ATldv_blast_assert.split_P19_34)) && !((hbv_main.ATldv_blast_assert.split_T8_45 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_K16_46)) && !((!hbv_main.ATldv_blast_assert.split_V4_207 || !hbv_main.ATldv_blast_assert.split_M4_208) && hbv_main.ATldv_blast_assert.split_V4_207)) && !((0 < hbv_main.ATldv_blast_assert.split_B11_222 && hbv_main.ATldv_blast_assert.split_O1_44) && hbv_main.ATldv_blast_assert.split_T10_431 <= 0)) && hbv_main.ATldv_blast_assert.split_K17_139 == hbv_main.ATldv_blast_assert.split_M8_426) && hbv_main.ATldv_blast_assert.split_L5_76 + 168 == hbv_main.ATldv_blast_assert.split_K4_257) && hbv_main.ATldv_blast_assert.split_E5_364 == hbv_main.ATldv_blast_assert.split_K5_365) && !(hbv_main.ATldv_blast_assert.split_J13_415 != hbv_main.ATldv_blast_assert.split_H13_201[hbv_main.ATldv_blast_assert.split_F13_414] && hbv_main.ATldv_blast_assert.split_J1_27)) && hbv_main.ATldv_blast_assert.split_J14_445 + 1 == hbv_main.ATldv_blast_assert.split_K14_268) && hbv_main.ATldv_blast_assert.split_S13_336 == hbv_main.ATldv_blast_assert.split_V14_250) && !(hbv_main.ATldv_blast_assert.split_O14_170 && (!hbv_main.ATldv_blast_assert.split_J1_27 || !hbv_main.ATldv_blast_assert.split_O14_170))) && !((!hbv_main.ATldv_blast_assert.split_L_450 || !hbv_main.ATldv_blast_assert.split_T16_210) && (hbv_main.ATldv_blast_assert.split_T16_210 || hbv_main.ATldv_blast_assert.split_L_450))) && hbv_main.ATldv_blast_assert.split_O12_9 == hbv_main.ATldv_blast_assert.split_N12_521 + 1) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_B4_505 != hbv_main.ATldv_blast_assert.split_Z3_454[hbv_main.ATldv_blast_assert.split_A4_470 := 8])) && !((0 < hbv_main.ATldv_blast_assert.split_D7_142 && hbv_main.ATldv_blast_assert.split_I4_52) && hbv_main.ATldv_blast_assert.split_N1_498 <= 0)) && hbv_main.ATldv_blast_assert.split_H17_28 == hbv_main.ATldv_blast_assert.split_T17_111) && hbv_main.ATldv_blast_assert.split_D5_252 == hbv_main.ATldv_blast_assert.split_I5_253) && !(hbv_main.ATldv_blast_assert.split_A2_121 != hbv_main.ATldv_blast_assert.split_W1_462[hbv_main.ATldv_blast_assert.split_X1_193 := 3] && hbv_main.ATldv_blast_assert.split_I4_52)) && hbv_main.ATldv_blast_assert.split_P11_388 == hbv_main.ATldv_blast_assert.split_B13_12 + 132) && hbv_main.ATldv_blast_assert.split_W14_330 == hbv_main.ATldv_blast_assert.split_V14_250) && !((hbv_main.ATldv_blast_assert.split_A3_233 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_O10_68 <= 0)) && !(((hbv_main.ATldv_blast_assert.split_V1_47 == 0 && hbv_main.ATldv_blast_assert.split_K3_312 != hbv_main.ATldv_blast_assert.split_L3_342) || (hbv_main.ATldv_blast_assert.split_L3_342 != hbv_main.ATldv_blast_assert.split_V1_47 && hbv_main.ATldv_blast_assert.split_K3_312 == 0)) && hbv_main.ATldv_blast_assert.split_I4_52)) && !((!hbv_main.ATldv_blast_assert.split_U14_437 && hbv_main.ATldv_blast_assert.split_C1_6) && hbv_main.ATldv_blast_assert.split_X14_145)) && hbv_main.ATldv_blast_assert.split_D19_391 == hbv_main.ATldv_blast_assert.split_G8_392) && !(hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_M13_36[hbv_main.ATldv_blast_assert.split_N13_322] != hbv_main.ATldv_blast_assert.split_K13_267)) && !((hbv_main.ATldv_blast_assert.split_W2_227 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && hbv_main.ATldv_blast_assert.split_E14_284 == hbv_main.ATldv_blast_assert.split_D15_285) && !((hbv_main.ATldv_blast_assert.split_O10_68 != 0 || !hbv_main.ATldv_blast_assert.split_K_423) && (hbv_main.ATldv_blast_assert.split_K_423 || hbv_main.ATldv_blast_assert.split_O10_68 == 0))) && !((hbv_main.ATldv_blast_assert.split_I13_87 <= 0 && 0 < hbv_main.ATldv_blast_assert.split_G13_86) && hbv_main.ATldv_blast_assert.split_J1_27)) && !(hbv_main.ATldv_blast_assert.split_D7_142 <= 0 && hbv_main.ATldv_blast_assert.split_R7_23)) && hbv_main.ATldv_blast_assert.split_C4_460 == 184 + hbv_main.ATldv_blast_assert.split_L5_76) && !(hbv_main.ATldv_blast_assert.split_G13_86 != hbv_main.ATldv_blast_assert.split_H13_201[hbv_main.ATldv_blast_assert.split_E1_37] && hbv_main.ATldv_blast_assert.split_J1_27)) && !((hbv_main.ATldv_blast_assert.split_X2_481 != 10 && hbv_main.ATldv_blast_assert.split_I4_52) && hbv_main.ATldv_blast_assert.split_T2_401 == 0)) && hbv_main.ATldv_blast_assert.split_K14_268 == hbv_main.ATldv_blast_assert.split_P14_269) && !((hbv_main.ATldv_blast_assert.split_K18_296 != hbv_main.ATldv_blast_assert.split_Y17_458 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_Z17_72)) && !(hbv_main.ATldv_blast_assert.split_D11_143 != hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_C11_223] && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_C_56 + 80 == hbv_main.ATldv_blast_assert.split_A3_233) && !((hbv_main.ATldv_blast_assert.split_F17_179 != hbv_main.ATldv_blast_assert.split_V16_206 && hbv_main.ATldv_blast_assert.split_W16_136) && hbv_main.ATldv_blast_assert.split_X16_135)) && !(hbv_main.ATldv_blast_assert.split_W1_462 != hbv_main.ATldv_blast_assert.split_T1_420[hbv_main.ATldv_blast_assert.split_U1_517 := hbv_main.ATldv_blast_assert.split_V1_240] && hbv_main.ATldv_blast_assert.split_I4_52)) && hbv_main.ATldv_blast_assert.split_N17_132 == hbv_main.ATldv_blast_assert.split_R_133) && hbv_main.ATldv_blast_assert.split_K1_430 == hbv_main.ATldv_blast_assert.split_D7_142 + 24) && hbv_main.ATldv_blast_assert.split_V7_261 == hbv_main.ATldv_blast_assert.split_Z7_435) && hbv_main.ATldv_blast_assert.split_M19_444 == hbv_main.ATldv_blast_assert.split_B19_299) && !(hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_I8_506)) && 112 + hbv_main.ATldv_blast_assert.split_Q5_326 == hbv_main.ATldv_blast_assert.split_S5_327) && !((!hbv_main.ATldv_blast_assert.split_T14_183 || hbv_main.ATldv_blast_assert.split_Q14_184 != 0) && (hbv_main.ATldv_blast_assert.split_T14_183 || hbv_main.ATldv_blast_assert.split_Q14_184 == 0))) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_B9_67 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && !((hbv_main.ATldv_blast_assert.split_A1_274 && hbv_main.ATldv_blast_assert.split_X_307) && hbv_main.ATldv_blast_assert.split_V_467)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_F9_456 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_K16_46)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_U1_517 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && hbv_main.ATldv_blast_assert.split_I3_311 * 32768 == hbv_main.ATldv_blast_assert.split_K3_312) && hbv_main.ATldv_blast_assert.split_Q2_276 == 552 + hbv_main.ATldv_blast_assert.split_C_56) && hbv_main.ATldv_blast_assert.split_H19_380 == hbv_main.ATldv_blast_assert.split_S19_510) && 560 + hbv_main.ATldv_blast_assert.split_O10_68 == hbv_main.ATldv_blast_assert.split_E10_309) && !((hbv_main.ATldv_blast_assert.split_V11_263 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_W11_146)) && hbv_main.ATldv_blast_assert.split_W11_146 + 1124 == hbv_main.ATldv_blast_assert.split_S9_171) && !((hbv_main.ATldv_blast_assert.split_Y14_144 != hbv_main.ATldv_blast_assert.split_A15_83 && hbv_main.ATldv_blast_assert.split_C1_6) && hbv_main.ATldv_blast_assert.split_X14_145)) && hbv_main.ATldv_blast_assert.split_T8_45 == hbv_main.ATldv_blast_assert.split_K16_46 + 24) && hbv_main.ATldv_blast_assert.split_O16_29 == hbv_main.ATldv_blast_assert.split_N16_500) && !(hbv_main.ATldv_blast_assert.split_W5_381[hbv_main.ATldv_blast_assert.split_B6_382] != hbv_main.ATldv_blast_assert.split_V5_356 && hbv_main.ATldv_blast_assert.split_L6_106)) && !((hbv_main.ATldv_blast_assert.split_X1_193 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && !(hbv_main.ATldv_blast_assert.split_H5_90 && hbv_main.ATldv_blast_assert.split_Z4_194[hbv_main.ATldv_blast_assert.split_K4_257 := hbv_main.ATldv_blast_assert.split_L4_258] != hbv_main.ATldv_blast_assert.split_D5_252)) && !(hbv_main.ATldv_blast_assert.split_P10_434 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_G4_177 <= 0)) && !((hbv_main.ATldv_blast_assert.split_E10_309 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && hbv_main.ATldv_blast_assert.split_J15_148 == hbv_main.ATldv_blast_assert.split_E15_149) && !((hbv_main.ATldv_blast_assert.split_I15_329 != hbv_main.ATldv_blast_assert.split_W14_330 && hbv_main.ATldv_blast_assert.split_C1_6) && hbv_main.ATldv_blast_assert.split_X14_145)) && !((hbv_main.ATldv_blast_assert.split_P15_113 && hbv_main.ATldv_blast_assert.split_F14_26) && !hbv_main.ATldv_blast_assert.split_G14_114)) && hbv_main.ATldv_blast_assert.split_R15_3 == hbv_main.ATldv_blast_assert.split_H15_407) && hbv_main.ATldv_blast_assert.split_E11_94 == 72 + hbv_main.ATldv_blast_assert.split_B13_12) && hbv_main.ATldv_blast_assert.split_M7_237 == hbv_main.ATldv_blast_assert.split_G7_251) && !((hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_F5_77) && hbv_main.ATldv_blast_assert.split_G5_225 != hbv_main.ATldv_blast_assert.split_M5_226)) && !(hbv_main.ATldv_blast_assert.split_A7_53 && hbv_main.ATldv_blast_assert.split_E1_409)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_J11_485 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && !((hbv_main.ATldv_blast_assert.split_B_55 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && hbv_main.ATldv_blast_assert.split_D11_143 == hbv_main.ATldv_blast_assert.split_O12_9) && !((hbv_main.ATldv_blast_assert.split_O14_170 && hbv_main.ATldv_blast_assert.split_W16_136) && hbv_main.ATldv_blast_assert.split_Q16_185 != hbv_main.ATldv_blast_assert.split_L14_337)) && !((hbv_main.ATldv_blast_assert.split_M12_338 && hbv_main.ATldv_blast_assert.split_L12_81) && hbv_main.ATldv_blast_assert.split_I12_80)) && !((0 < hbv_main.ATldv_blast_assert.split_D7_142 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_O5_198 <= 0)) && hbv_main.ATldv_blast_assert.split_R3_427 == hbv_main.ATldv_blast_assert.split_P3_316) && hbv_main.ATldv_blast_assert.split_X11_404 == hbv_main.ATldv_blast_assert.split_V11_263) && 108 + hbv_main.ATldv_blast_assert.split_V11_263 == hbv_main.ATldv_blast_assert.split_W11_146) && hbv_main.ATldv_blast_assert.split_J19_162 == hbv_main.ATldv_blast_assert.split_Z18_244) && hbv_main.ATldv_blast_assert.split_F13_414 == hbv_main.ATldv_blast_assert.split_E13_402) && hbv_main.ATldv_blast_assert.split_Y7_262 == hbv_main.ATldv_blast_assert.split_D8_290) && !(((!hbv_main.ATldv_blast_assert.split_G12_78 || !hbv_main.ATldv_blast_assert.split_F12_79) && (!hbv_main.ATldv_blast_assert.split_I12_80 || !hbv_main.ATldv_blast_assert.split_L12_81)) && hbv_main.ATldv_blast_assert.split_J12_82)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_M2_377 != hbv_main.ATldv_blast_assert.split_K2_318[hbv_main.ATldv_blast_assert.split_J2_468])) && !((hbv_main.ATldv_blast_assert.split_M5_226 != hbv_main.ATldv_blast_assert.split_I5_253 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_H5_90)) && hbv_main.ATldv_blast_assert.split_W11_146 == hbv_main.ATldv_blast_assert.split_H11_116 + 136) && !((hbv_main.ATldv_blast_assert.split_K18_296 != hbv_main.ATldv_blast_assert.split_C18_475 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_D18_150)) && !(hbv_main.ATldv_blast_assert.split_L5_76 <= 0 && hbv_main.ATldv_blast_assert.split_J5_224)) && hbv_main.ATldv_blast_assert.split_N17_132 == hbv_main.ATldv_blast_assert.split_U17_297) && !(hbv_main.ATldv_blast_assert.split_Q18_461 && hbv_main.ATldv_blast_assert.split_T18_119)) && !((hbv_main.ATldv_blast_assert.split_Q2_276 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && !(((hbv_main.ATldv_blast_assert.split_H_51 == 0 && hbv_main.ATldv_blast_assert.split_Z10_230 != hbv_main.ATldv_blast_assert.split_A11_520) || (hbv_main.ATldv_blast_assert.split_Z10_230 == 0 && hbv_main.ATldv_blast_assert.split_H_51 != hbv_main.ATldv_blast_assert.split_A11_520)) && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_T10_431] != hbv_main.ATldv_blast_assert.split_U10_249)) && !((hbv_main.ATldv_blast_assert.split_A1_274 && hbv_main.ATldv_blast_assert.split_B1_308) && !hbv_main.ATldv_blast_assert.split_V_467)) && !((!hbv_main.ATldv_blast_assert.split_V18_161 && hbv_main.ATldv_blast_assert.split_U18_134) && hbv_main.ATldv_blast_assert.split_T18_119)) && !(hbv_main.ATldv_blast_assert.split_L5_76 <= 0 && hbv_main.ATldv_blast_assert.split_L6_106)) && hbv_main.ATldv_blast_assert.split_B13_12 + 168 == hbv_main.ATldv_blast_assert.split_K12_513) && hbv_main.ATldv_blast_assert.split_Z2_232 == hbv_main.ATldv_blast_assert.split_A3_233) && hbv_main.ATldv_blast_assert.split_O6_138 == hbv_main.ATldv_blast_assert.split_I7_158) && !((hbv_main.ATldv_blast_assert.split_J8_273 && hbv_main.ATldv_blast_assert.split_A1_274) && hbv_main.ATldv_blast_assert.split_S3_271 != hbv_main.ATldv_blast_assert.split_O_272)) && !((hbv_main.ATldv_blast_assert.split_K19_372 != hbv_main.ATldv_blast_assert.split_X19_246 && hbv_main.ATldv_blast_assert.split_L19_109) && hbv_main.ATldv_blast_assert.split_D20_35)) && !((hbv_main.ATldv_blast_assert.split_G6_499 != 0 || !hbv_main.ATldv_blast_assert.split_H6_110) && (hbv_main.ATldv_blast_assert.split_G6_499 == 0 || hbv_main.ATldv_blast_assert.split_H6_110))) && !((hbv_main.ATldv_blast_assert.split_E17_218 != hbv_main.ATldv_blast_assert.split_Z16_270 && hbv_main.ATldv_blast_assert.split_C17_181) && hbv_main.ATldv_blast_assert.split_B17_182)) && !((0 < hbv_main.ATldv_blast_assert.split_D7_142 && hbv_main.ATldv_blast_assert.split_K1_430 <= 0) && hbv_main.ATldv_blast_assert.split_I4_52)) && !((hbv_main.ATldv_blast_assert.split_V_467 || hbv_main.ATldv_blast_assert.split_U_480 == 0) && (hbv_main.ATldv_blast_assert.split_U_480 != 0 || !hbv_main.ATldv_blast_assert.split_V_467))) && hbv_main.ATldv_blast_assert.split_N15_189 == hbv_main.ATldv_blast_assert.split_E15_149) && !((!hbv_main.ATldv_blast_assert.split_E20_228 || !hbv_main.ATldv_blast_assert.split_D20_35) && hbv_main.ATldv_blast_assert.split_E20_228)) && !((hbv_main.ATldv_blast_assert.split_V7_261 != hbv_main.ATldv_blast_assert.split_N7_219 && hbv_main.ATldv_blast_assert.split_O7_103) && hbv_main.ATldv_blast_assert.split_C8_239)) && !(hbv_main.ATldv_blast_assert.split_T19_191 && hbv_main.ATldv_blast_assert.split_X18_289)) && 32 + hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_Z_49) && hbv_main.ATldv_blast_assert.split_E19_479 == hbv_main.ATldv_blast_assert.split_T1_32) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_L2_236 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && hbv_main.ATldv_blast_assert.split_I7_158 == hbv_main.ATldv_blast_assert.split_E6_298) && !(hbv_main.ATldv_blast_assert.split_L5_76 != hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_B6_382] && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_F12_79 && (!hbv_main.ATldv_blast_assert.split_C12_432 || !hbv_main.ATldv_blast_assert.split_F12_79))) && hbv_main.ATldv_blast_assert.split_D19_391 == hbv_main.ATldv_blast_assert.split_O19_417) && !(hbv_main.ATldv_blast_assert.split_A7_53 && hbv_main.ATldv_blast_assert.split_H17_28[hbv_main.ATldv_blast_assert.split_T7_255 := hbv_main.ATldv_blast_assert.split_D1_408] != hbv_main.ATldv_blast_assert.split_E7_20)) && hbv_main.ATldv_blast_assert.split_O17_130 == hbv_main.ATldv_blast_assert.split_O8_387) && !((hbv_main.ATldv_blast_assert.split_F14_26 && hbv_main.ATldv_blast_assert.split_J1_27) && hbv_main.ATldv_blast_assert.split_R13_24 != hbv_main.ATldv_blast_assert.split_T13_25)) && hbv_main.ATldv_blast_assert.split_L17_85 == hbv_main.ATldv_blast_assert.split_A18_428) && hbv_main.ATldv_blast_assert.split_A13_125 == hbv_main.ATldv_blast_assert.split_U12_16) && !((hbv_main.ATldv_blast_assert.split_C16_168 && hbv_main.ATldv_blast_assert.split_I16_421) && hbv_main.ATldv_blast_assert.split_S_5)) && !(hbv_main.ATldv_blast_assert.split_C13_199[hbv_main.ATldv_blast_assert.split_D13_200 := -1] != hbv_main.ATldv_blast_assert.split_H13_201 && hbv_main.ATldv_blast_assert.split_J1_27)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_E12_339 != hbv_main.ATldv_blast_assert.split_P12_13[hbv_main.ATldv_blast_assert.split_X11_404])) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_E_58 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && hbv_main.ATldv_blast_assert.split_E14_284 + 1 == hbv_main.ATldv_blast_assert.split_D14_292) && !((!hbv_main.ATldv_blast_assert.split_L19_109 || !hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_L19_109)) && hbv_main.ATldv_blast_assert.split_V5_356 + 100 == hbv_main.ATldv_blast_assert.split_X5_357) && hbv_main.ATldv_blast_assert.split_P7_412 == hbv_main.ATldv_blast_assert.split_I7_158) && hbv_main.ATldv_blast_assert.split_E3_264 == 2 + hbv_main.ATldv_blast_assert.split_M3_175) && hbv_main.ATldv_blast_assert.split_T10_431 == 2 + hbv_main.ATldv_blast_assert.split_B11_222) && hbv_main.ATldv_blast_assert.split_O10_68 == hbv_main.ATldv_blast_assert.split_B9_67) && hbv_main.ATldv_blast_assert.split_R_133 + 1 == hbv_main.ATldv_blast_assert.split_S_160) && !(hbv_main.ATldv_blast_assert.split_H18_31 && (!hbv_main.ATldv_blast_assert.split_H18_31 || !hbv_main.ATldv_blast_assert.split_L16_197))) && 88 + hbv_main.ATldv_blast_assert.split_B13_12 == hbv_main.ATldv_blast_assert.split_J11_485) && hbv_main.ATldv_blast_assert.split_X_1 == hbv_main.ATldv_blast_assert.split_Q_2) && !((5 != hbv_main.ATldv_blast_assert.split_O4_196 || !hbv_main.ATldv_blast_assert.split_R4_215) && (5 == hbv_main.ATldv_blast_assert.split_O4_196 || hbv_main.ATldv_blast_assert.split_R4_215))) && hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_V14_250) && !((hbv_main.ATldv_blast_assert.split_I9_241 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_W11_146)) && !(!hbv_main.ATldv_blast_assert.split_D12_487 && hbv_main.ATldv_blast_assert.split_E12_339 < 5)) && !(hbv_main.ATldv_blast_assert.split_F14_26 && (!hbv_main.ATldv_blast_assert.split_J1_27 || !hbv_main.ATldv_blast_assert.split_F14_26))) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_L1_495[hbv_main.ATldv_blast_assert.split_M1_429 := hbv_main.ATldv_blast_assert.split_S3_271] != hbv_main.ATldv_blast_assert.split_O1_515)) && hbv_main.ATldv_blast_assert.split_C14_293 == hbv_main.ATldv_blast_assert.split_X13_346) && hbv_main.ATldv_blast_assert.split_O8_387 + 1 == hbv_main.ATldv_blast_assert.split_P8_433) && !((hbv_main.ATldv_blast_assert.split_O7_103 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_X7_234 != hbv_main.ATldv_blast_assert.split_P7_412)) && !((hbv_main.ATldv_blast_assert.split_M18_361 != hbv_main.ATldv_blast_assert.split_G19_362 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_T18_119)) && hbv_main.ATldv_blast_assert.split_K17_139 == hbv_main.ATldv_blast_assert.split_C18_475) && !((!hbv_main.ATldv_blast_assert.split_I14_416 && hbv_main.ATldv_blast_assert.split_O14_170) && hbv_main.ATldv_blast_assert.split_J1_27)) && !(hbv_main.ATldv_blast_assert.split_U6_88 && !hbv_main.ATldv_blast_assert.split_T6_89)) && hbv_main.ATldv_blast_assert.split_I18_328 == hbv_main.ATldv_blast_assert.split_O17_130) && !((hbv_main.ATldv_blast_assert.split_O1_44 && 0 < hbv_main.ATldv_blast_assert.split_O10_68) && hbv_main.ATldv_blast_assert.split_Y9_310 <= 0)) && !((hbv_main.ATldv_blast_assert.split_E13_402 <= 0 && hbv_main.ATldv_blast_assert.split_J1_27) && 0 < hbv_main.ATldv_blast_assert.split_K16_46)) && !(hbv_main.ATldv_blast_assert.split_C1_6 && hbv_main.ATldv_blast_assert.split_B15_451[hbv_main.ATldv_blast_assert.split_C15_503 := 0] != hbv_main.ATldv_blast_assert.split_H15_407)) && !((hbv_main.ATldv_blast_assert.split_G4_177 != hbv_main.ATldv_blast_assert.split_P_147 && hbv_main.ATldv_blast_assert.split_J8_273) && hbv_main.ATldv_blast_assert.split_A1_274)) && !(hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_M13_36[hbv_main.ATldv_blast_assert.split_N13_322 := hbv_main.ATldv_blast_assert.split_O13_266] != hbv_main.ATldv_blast_assert.split_E15_149)) && !((hbv_main.ATldv_blast_assert.split_F14_26 && hbv_main.ATldv_blast_assert.split_G14_114) && hbv_main.ATldv_blast_assert.split_A14_295)) && !((hbv_main.ATldv_blast_assert.split_Z17_72 && (!hbv_main.ATldv_blast_assert.split_A16_291 || !hbv_main.ATldv_blast_assert.split_Z17_72)) && (!hbv_main.ATldv_blast_assert.split_D16_167 || !hbv_main.ATldv_blast_assert.split_C16_168))) && hbv_main.ATldv_blast_assert.split_H7_128 == hbv_main.ATldv_blast_assert.split_N7_219) && hbv_main.ATldv_blast_assert.split_P3_316 == 72 + hbv_main.ATldv_blast_assert.split_L5_76) && hbv_main.ATldv_blast_assert.split_N17_132 == hbv_main.ATldv_blast_assert.split_L8_302) && !((hbv_main.ATldv_blast_assert.split_P3_316 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_R11_62 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && hbv_main.ATldv_blast_assert.split_C15_503 == hbv_main.ATldv_blast_assert.split_Z14_504) && !(hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_F8_320)) && !((hbv_main.ATldv_blast_assert.split_J10_333 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && !((!hbv_main.ATldv_blast_assert.split_H12_203 && hbv_main.ATldv_blast_assert.split_F12_79) && hbv_main.ATldv_blast_assert.split_X12_204)) && !((hbv_main.ATldv_blast_assert.split_S4_212 && hbv_main.ATldv_blast_assert.split_V4_207) && hbv_main.ATldv_blast_assert.split_W4_411)) && !(hbv_main.ATldv_blast_assert.split_G8_392 <= 0 && hbv_main.ATldv_blast_assert.split_H8_449)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_S2_242 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && hbv_main.ATldv_blast_assert.split_F15_100 == hbv_main.ATldv_blast_assert.split_O15_331) && !((hbv_main.ATldv_blast_assert.split_T19_191 && (!hbv_main.ATldv_blast_assert.split_T18_119 || !hbv_main.ATldv_blast_assert.split_U18_134)) && (!hbv_main.ATldv_blast_assert.split_T19_191 || !hbv_main.ATldv_blast_assert.split_S18_403))) && !((!hbv_main.ATldv_blast_assert.split_I14_416 || hbv_main.ATldv_blast_assert.split_P13_440 != 0) && (hbv_main.ATldv_blast_assert.split_I14_416 || hbv_main.ATldv_blast_assert.split_P13_440 == 0))) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_R17_396) && hbv_main.ATldv_blast_assert.split_K18_296 != hbv_main.ATldv_blast_assert.split_Q17_464)) && !((hbv_main.ATldv_blast_assert.split_R7_23 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_V7_261 != hbv_main.ATldv_blast_assert.split_Q7_156)) && hbv_main.ATldv_blast_assert.split_G15_7 == hbv_main.ATldv_blast_assert.split_M15_8) && !((hbv_main.ATldv_blast_assert.split_W15_501 == 0 || hbv_main.ATldv_blast_assert.split_I16_421) && (!hbv_main.ATldv_blast_assert.split_I16_421 || hbv_main.ATldv_blast_assert.split_W15_501 != 0))) && !(hbv_main.ATldv_blast_assert.split_Y15_399 && hbv_main.ATldv_blast_assert.split_Z15_301 <= 0)) && !((hbv_main.ATldv_blast_assert.split_G6_499 != hbv_main.ATldv_blast_assert.split_F6_260 && hbv_main.ATldv_blast_assert.split_L19_109) && hbv_main.ATldv_blast_assert.split_L6_106)) && !(hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_M13_36[hbv_main.ATldv_blast_assert.split_E1_37] != hbv_main.ATldv_blast_assert.split_V_38)) && 30 + hbv_main.ATldv_blast_assert.split_C_56 == hbv_main.ATldv_blast_assert.split_L2_236) && !(hbv_main.ATldv_blast_assert.split_X16_135 && !hbv_main.ATldv_blast_assert.split_W16_136)) && !((!hbv_main.ATldv_blast_assert.split_L16_197 || !hbv_main.ATldv_blast_assert.split_X14_145) && hbv_main.ATldv_blast_assert.split_X14_145)) && !(hbv_main.ATldv_blast_assert.split_R10_366 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_B18_335 == hbv_main.ATldv_blast_assert.split_J17_4) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_V17_112) && hbv_main.ATldv_blast_assert.split_J18_69 != hbv_main.ATldv_blast_assert.split_T17_111)) && !(hbv_main.ATldv_blast_assert.split_A10_340[hbv_main.ATldv_blast_assert.split_B10_126 := hbv_main.ATldv_blast_assert.split_C10_277] != hbv_main.ATldv_blast_assert.split_D10_341 && hbv_main.ATldv_blast_assert.split_O1_44)) && !((hbv_main.ATldv_blast_assert.split_O14_170 && hbv_main.ATldv_blast_assert.split_W16_136) && hbv_main.ATldv_blast_assert.split_S16_169 != hbv_main.ATldv_blast_assert.split_N14_101)) && 112 + hbv_main.ATldv_blast_assert.split_G13_86 == hbv_main.ATldv_blast_assert.split_I13_87) && !((hbv_main.ATldv_blast_assert.split_U5_447 == 0 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_Y5_413 != 4)) && !((!hbv_main.ATldv_blast_assert.split_K8_360 && hbv_main.ATldv_blast_assert.split_B17_182) && hbv_main.ATldv_blast_assert.split_J8_273)) && !((hbv_main.ATldv_blast_assert.split_Z6_104 || hbv_main.ATldv_blast_assert.split_N6_259 == 0) && (hbv_main.ATldv_blast_assert.split_N6_259 != 0 || !hbv_main.ATldv_blast_assert.split_Z6_104))) && hbv_main.ATldv_blast_assert.split_X1_193 == hbv_main.ATldv_blast_assert.split_C_56 + 24) && !((!hbv_main.ATldv_blast_assert.split_I16_421 && hbv_main.ATldv_blast_assert.split_D18_150) && hbv_main.ATldv_blast_assert.split_S_5)) && hbv_main.ATldv_blast_assert.split_Y9_310 == 840 + hbv_main.ATldv_blast_assert.split_O10_68) && !((hbv_main.ATldv_blast_assert.split_U13_202 != 0 || !hbv_main.ATldv_blast_assert.split_G14_114) && (hbv_main.ATldv_blast_assert.split_G14_114 || hbv_main.ATldv_blast_assert.split_U13_202 == 0))) && hbv_main.ATldv_blast_assert.split_C_56 + 28 == hbv_main.ATldv_blast_assert.split_G2_216) && !((((((!hbv_main.ATldv_blast_assert.split_R17_396 || !hbv_main.ATldv_blast_assert.split_O18_71) && (!hbv_main.ATldv_blast_assert.split_Z17_72 || !hbv_main.ATldv_blast_assert.split_O18_71)) && hbv_main.ATldv_blast_assert.split_O18_71) && (!hbv_main.ATldv_blast_assert.split_H18_31 || !hbv_main.ATldv_blast_assert.split_O18_71)) && (!hbv_main.ATldv_blast_assert.split_D18_150 || !hbv_main.ATldv_blast_assert.split_O18_71)) && (!hbv_main.ATldv_blast_assert.split_V17_112 || !hbv_main.ATldv_blast_assert.split_O18_71))) && !(hbv_main.ATldv_blast_assert.split_A15_83 <= 0 && hbv_main.ATldv_blast_assert.split_C1_6)) && !((hbv_main.ATldv_blast_assert.split_R1_92 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && hbv_main.ATldv_blast_assert.split_H19_380 == hbv_main.ATldv_blast_assert.split_W18_466) && !((hbv_main.ATldv_blast_assert.split_Y19_245 != hbv_main.ATldv_blast_assert.split_X19_246 && hbv_main.ATldv_blast_assert.split_Z19_247) && hbv_main.ATldv_blast_assert.split_A20_248)) && !(((hbv_main.ATldv_blast_assert.split_C8_239 && (!hbv_main.ATldv_blast_assert.split_C8_239 || !hbv_main.ATldv_blast_assert.split_R7_23)) && (!hbv_main.ATldv_blast_assert.split_C8_239 || !hbv_main.ATldv_blast_assert.split_O7_103)) && (!hbv_main.ATldv_blast_assert.split_C8_239 || !hbv_main.ATldv_blast_assert.split_L7_238))) && hbv_main.ATldv_blast_assert.split_H19_380 == hbv_main.ATldv_blast_assert.split_Y19_245) && !((hbv_main.ATldv_blast_assert.split_F12_79 && hbv_main.ATldv_blast_assert.split_H12_203) && hbv_main.ATldv_blast_assert.split_G12_78)) && !((hbv_main.ATldv_blast_assert.split_U14_437 && hbv_main.ATldv_blast_assert.split_O1_44) && hbv_main.ATldv_blast_assert.split_X14_145)) && hbv_main.ATldv_blast_assert.split_R16_205 == hbv_main.ATldv_blast_assert.split_V16_206) && !(!hbv_main.ATldv_blast_assert.split_L12_81 && hbv_main.ATldv_blast_assert.split_I12_80)) && hbv_main.ATldv_blast_assert.split_Z14_504 == 32 + hbv_main.ATldv_blast_assert.split_A15_83) && 256 * hbv_main.ATldv_blast_assert.split_W10_50 == hbv_main.ATldv_blast_assert.split_H_51) && !(hbv_main.ATldv_blast_assert.split_J8_273 && hbv_main.ATldv_blast_assert.split_H17_28[hbv_main.ATldv_blast_assert.split_I_469] != hbv_main.ATldv_blast_assert.split_W11_146)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_U9_371[hbv_main.ATldv_blast_assert.split_T9_477] != hbv_main.ATldv_blast_assert.split_W9_471)) && !((hbv_main.ATldv_blast_assert.split_T1_32 != hbv_main.ATldv_blast_assert.split_B20_33 && hbv_main.ATldv_blast_assert.split_P19_34) && hbv_main.ATldv_blast_assert.split_D20_35)) && hbv_main.ATldv_blast_assert.split_D17_375 == hbv_main.ATldv_blast_assert.split_O17_130) && !((hbv_main.ATldv_blast_assert.split_C17_181 && hbv_main.ATldv_blast_assert.split_B17_182) && !hbv_main.ATldv_blast_assert.split_T16_210)) && hbv_main.ATldv_blast_assert.split_S3_271 == hbv_main.ATldv_blast_assert.split_G3_406) && hbv_main.ATldv_blast_assert.split_J17_4 == hbv_main.ATldv_blast_assert.split_X17_70) && hbv_main.ATldv_blast_assert.split_G5_225 == hbv_main.ATldv_blast_assert.split_C5_463) && !((hbv_main.ATldv_blast_assert.split_W18_466 == 0 || hbv_main.ATldv_blast_assert.split_X18_289) && (hbv_main.ATldv_blast_assert.split_W18_466 != 0 || !hbv_main.ATldv_blast_assert.split_X18_289))) && hbv_main.ATldv_blast_assert.split_L1_18 == hbv_main.ATldv_blast_assert.split_M10_164) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_N2_378[hbv_main.ATldv_blast_assert.split_B_55 := hbv_main.ATldv_blast_assert.split_Z9_519] != hbv_main.ATldv_blast_assert.split_P2_275)) && hbv_main.ATldv_blast_assert.split_O10_68 + 28 == hbv_main.ATldv_blast_assert.split_Q9_211) && !(!hbv_main.ATldv_blast_assert.split_P6_153 && 0 < hbv_main.ATldv_blast_assert.split_Q6_483)) && !(hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_H8_449)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_L9_410 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && !(hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_E3_264] != hbv_main.ATldv_blast_assert.split_F3_422 && hbv_main.ATldv_blast_assert.split_I4_52)) && hbv_main.ATldv_blast_assert.split_Z8_511 == hbv_main.ATldv_blast_assert.split_S1_419) && hbv_main.ATldv_blast_assert.split_E_58 == 104 + hbv_main.ATldv_blast_assert.split_B13_12) && !(hbv_main.ATldv_blast_assert.split_R2_278[hbv_main.ATldv_blast_assert.split_S2_242 := hbv_main.ATldv_blast_assert.split_F10_523] != hbv_main.ATldv_blast_assert.split_V2_400 && hbv_main.ATldv_blast_assert.split_I4_52)) && !((!hbv_main.ATldv_blast_assert.split_A1_274 || !hbv_main.ATldv_blast_assert.split_J8_273) && hbv_main.ATldv_blast_assert.split_A1_274)) && !((!hbv_main.ATldv_blast_assert.split_Y6_102 || !hbv_main.ATldv_blast_assert.split_T6_89) && hbv_main.ATldv_blast_assert.split_T6_89)) && hbv_main.ATldv_blast_assert.split_S15_231 == hbv_main.ATldv_blast_assert.split_O17_130) && hbv_main.ATldv_blast_assert.split_Y12_265 == hbv_main.ATldv_blast_assert.split_T12_478) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_G11_93 := hbv_main.ATldv_blast_assert.split_H11_116] != hbv_main.ATldv_blast_assert.split_I11_117)) && hbv_main.ATldv_blast_assert.split_W8_107 == hbv_main.ATldv_blast_assert.split_Y8_108) && !((hbv_main.ATldv_blast_assert.split_A12_395 <= 0 && hbv_main.ATldv_blast_assert.split_X12_204) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && !(hbv_main.ATldv_blast_assert.split_A14_295 && (!hbv_main.ATldv_blast_assert.split_A14_295 || !hbv_main.ATldv_blast_assert.split_F14_26))) && !((hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_Z7_435 != hbv_main.ATldv_blast_assert.split_C19_221)) && hbv_main.ATldv_blast_assert.split_W6_155 == hbv_main.ATldv_blast_assert.split_X6_379 + 1) && !(((((!hbv_main.ATldv_blast_assert.split_A20_248 || !hbv_main.ATldv_blast_assert.split_Z19_247) && (!hbv_main.ATldv_blast_assert.split_D20_35 || !hbv_main.ATldv_blast_assert.split_T19_191)) && hbv_main.ATldv_blast_assert.split_D20_35) && (!hbv_main.ATldv_blast_assert.split_D20_35 || !hbv_main.ATldv_blast_assert.split_P19_34)) && (!hbv_main.ATldv_blast_assert.split_L19_109 || !hbv_main.ATldv_blast_assert.split_D20_35))) && !(hbv_main.ATldv_blast_assert.split_M1_17 && hbv_main.ATldv_blast_assert.split_P12_13[hbv_main.ATldv_blast_assert.split_Q12_14 := hbv_main.ATldv_blast_assert.split_Q1_15] != hbv_main.ATldv_blast_assert.split_U12_16)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_E11_94 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && !((0 < hbv_main.ATldv_blast_assert.split_V_38 && hbv_main.ATldv_blast_assert.split_J1_27) && hbv_main.ATldv_blast_assert.split_N13_322 <= 0)) && !((!hbv_main.ATldv_blast_assert.split_S_5 || !hbv_main.ATldv_blast_assert.split_C16_168) && hbv_main.ATldv_blast_assert.split_C16_168)) && !(hbv_main.ATldv_blast_assert.split_D16_167 && !hbv_main.ATldv_blast_assert.split_C16_168)) && !(hbv_main.ATldv_blast_assert.split_J8_273 && (!hbv_main.ATldv_blast_assert.split_H_314 || !hbv_main.ATldv_blast_assert.split_J8_273))) && !(hbv_main.ATldv_blast_assert.split_U2_482 != hbv_main.ATldv_blast_assert.split_V2_400[hbv_main.ATldv_blast_assert.split_W2_227 := hbv_main.ATldv_blast_assert.split_X2_481] && hbv_main.ATldv_blast_assert.split_I4_52)) && hbv_main.ATldv_blast_assert.split_H7_128 == hbv_main.ATldv_blast_assert.split_C6_390) && !(hbv_main.ATldv_blast_assert.split_M1_17 && hbv_main.ATldv_blast_assert.split_B13_12 <= 0)) && hbv_main.ATldv_blast_assert.split_L5_76 + 168 == hbv_main.ATldv_blast_assert.split_A5_243) && !(hbv_main.ATldv_blast_assert.split_F5_77 && hbv_main.ATldv_blast_assert.split_Z4_194[hbv_main.ATldv_blast_assert.split_U4_127 := hbv_main.ATldv_blast_assert.split_Y4_66] != hbv_main.ATldv_blast_assert.split_C5_463)) && !(hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_Q10_394] != hbv_main.ATldv_blast_assert.split_R10_366 && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_I10_332[hbv_main.ATldv_blast_assert.split_J10_333] != hbv_main.ATldv_blast_assert.split_G10_334 && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_B13_12 + 168 == hbv_main.ATldv_blast_assert.split_A12_395) && !(hbv_main.ATldv_blast_assert.split_Q11_61[hbv_main.ATldv_blast_assert.split_R11_62 := hbv_main.ATldv_blast_assert.split_S11_63] != hbv_main.ATldv_blast_assert.split_T11_64 && hbv_main.ATldv_blast_assert.split_O1_44)) && !(5 <= hbv_main.ATldv_blast_assert.split_O4_196 && hbv_main.ATldv_blast_assert.split_N4_209)) && hbv_main.ATldv_blast_assert.split_I17_303 == hbv_main.ATldv_blast_assert.split_Y17_458) && !((hbv_main.ATldv_blast_assert.split_R6_152 && hbv_main.ATldv_blast_assert.split_T6_89) && hbv_main.ATldv_blast_assert.split_P6_153)) && !((!hbv_main.ATldv_blast_assert.split_T18_119 || !hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_T18_119)) && !(hbv_main.ATldv_blast_assert.split_X_307 && (!hbv_main.ATldv_blast_assert.split_X_307 || !hbv_main.ATldv_blast_assert.split_A1_274))) && !((hbv_main.ATldv_blast_assert.split_D1_408 != 0 || !hbv_main.ATldv_blast_assert.split_E1_409) && (hbv_main.ATldv_blast_assert.split_D1_408 == 0 || hbv_main.ATldv_blast_assert.split_E1_409))) && !(hbv_main.ATldv_blast_assert.split_F2_124 != hbv_main.ATldv_blast_assert.split_A2_121[hbv_main.ATldv_blast_assert.split_B2_122 := hbv_main.ATldv_blast_assert.split_C2_123] && hbv_main.ATldv_blast_assert.split_I4_52)) && !((hbv_main.ATldv_blast_assert.split_D20_35 && hbv_main.ATldv_blast_assert.split_T19_191) && hbv_main.ATldv_blast_assert.split_S19_510 != hbv_main.ATldv_blast_assert.split_X19_246)) && hbv_main.ATldv_blast_assert.split_O12_9 == hbv_main.ATldv_blast_assert.split_Z11_10 + 1) && !(hbv_main.ATldv_blast_assert.split_W3_99[hbv_main.ATldv_blast_assert.split_X3_178 := hbv_main.ATldv_blast_assert.split_Y3_256] != hbv_main.ATldv_blast_assert.split_Z3_454 && hbv_main.ATldv_blast_assert.split_I4_52)) && hbv_main.ATldv_blast_assert.split_O10_68 + 26 == hbv_main.ATldv_blast_assert.split_L9_410) && !((hbv_main.ATldv_blast_assert.split_J8_273 && hbv_main.ATldv_blast_assert.split_A1_274) && hbv_main.ATldv_blast_assert.split_C_56 != hbv_main.ATldv_blast_assert.split_M_509)) && !(!hbv_main.ATldv_blast_assert.split_V4_207 && hbv_main.ATldv_blast_assert.split_S4_212)) && !((hbv_main.ATldv_blast_assert.split_L6_106 && 0 < hbv_main.ATldv_blast_assert.split_V5_356) && hbv_main.ATldv_blast_assert.split_X5_357 <= 0)) && !(hbv_main.ATldv_blast_assert.split_H2_317 != hbv_main.ATldv_blast_assert.split_F2_124[hbv_main.ATldv_blast_assert.split_E2_39] && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_Z4_194[hbv_main.ATldv_blast_assert.split_H4_195] != hbv_main.ATldv_blast_assert.split_O4_196)) && !((hbv_main.ATldv_blast_assert.split_F_315 && hbv_main.ATldv_blast_assert.split_G_313) && hbv_main.ATldv_blast_assert.split_D_389)) && hbv_main.ATldv_blast_assert.split_K19_372 == hbv_main.ATldv_blast_assert.split_A19_476) && !((hbv_main.ATldv_blast_assert.split_L15_323 && (!hbv_main.ATldv_blast_assert.split_Y13_352 || !hbv_main.ATldv_blast_assert.split_L15_323)) && (!hbv_main.ATldv_blast_assert.split_A14_295 || !hbv_main.ATldv_blast_assert.split_B14_294))) && hbv_main.ATldv_blast_assert.split_Y1_176 == 1120 + hbv_main.ATldv_blast_assert.split_G4_177) && !(hbv_main.ATldv_blast_assert.split_B2_11 && hbv_main.ATldv_blast_assert.split_B13_12 <= 0)) && !((hbv_main.ATldv_blast_assert.split_A6_358 || hbv_main.ATldv_blast_assert.split_Z5_359 == 0) && (hbv_main.ATldv_blast_assert.split_Z5_359 != 0 || !hbv_main.ATldv_blast_assert.split_A6_358))) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_A10_340 != hbv_main.ATldv_blast_assert.split_X9_472[hbv_main.ATldv_blast_assert.split_Y9_310 := hbv_main.ATldv_blast_assert.split_Z9_519])) && hbv_main.ATldv_blast_assert.split_K18_296 == hbv_main.ATldv_blast_assert.split_N18_363) && hbv_main.ATldv_blast_assert.split_I19_118 == hbv_main.ATldv_blast_assert.split_C20_457) && !(!hbv_main.ATldv_blast_assert.split_J6_305 && 0 < hbv_main.ATldv_blast_assert.split_I6_306)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_B15_451[hbv_main.ATldv_blast_assert.split_R8_452 := hbv_main.ATldv_blast_assert.split_S8_438] != hbv_main.ATldv_blast_assert.split_U8_343)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_X8_344[hbv_main.ATldv_blast_assert.split_Y8_108 := hbv_main.ATldv_blast_assert.split_O10_68] != hbv_main.ATldv_blast_assert.split_A9_384)) && !((hbv_main.ATldv_blast_assert.split_N3_174 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_M3_175)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_A7_53) && hbv_main.ATldv_blast_assert.split_B7_54)) && hbv_main.ATldv_blast_assert.split_L14_337 == hbv_main.ATldv_blast_assert.split_E15_149) && !((hbv_main.ATldv_blast_assert.split_C16_168 && hbv_main.ATldv_blast_assert.split_Y15_399) && hbv_main.ATldv_blast_assert.split_A16_291)) && hbv_main.ATldv_blast_assert.split_S12_502 == hbv_main.ATldv_blast_assert.split_W12_300) && !(hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_R5_280 != hbv_main.ATldv_blast_assert.split_M5_226[hbv_main.ATldv_blast_assert.split_N5_105 := -1])) && hbv_main.ATldv_blast_assert.split_H11_116 == hbv_main.ATldv_blast_assert.split_V10_512) && hbv_main.ATldv_blast_assert.split_R19_488 == hbv_main.ATldv_blast_assert.split_G19_362) && hbv_main.ATldv_blast_assert.split_Y4_66 == hbv_main.ATldv_blast_assert.split_J4_75 + 1) && hbv_main.ATldv_blast_assert.split_Z1_354 == hbv_main.ATldv_blast_assert.split_Y1_176) && !((!hbv_main.ATldv_blast_assert.split_J12_82 || !hbv_main.ATldv_blast_assert.split_B2_11) && hbv_main.ATldv_blast_assert.split_B2_11)) && hbv_main.ATldv_blast_assert.split_I1_493 == hbv_main.ATldv_blast_assert.split_H1_141) && hbv_main.ATldv_blast_assert.split_F15_100 == hbv_main.ATldv_blast_assert.split_X13_346) && !((hbv_main.ATldv_blast_assert.split_J5_224 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_M5_226 != hbv_main.ATldv_blast_assert.split_K5_365)) && !((hbv_main.ATldv_blast_assert.split_E4_120 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && !((hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_X12_204) && hbv_main.ATldv_blast_assert.split_C13_199 != hbv_main.ATldv_blast_assert.split_Y12_265)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_B13_12 <= 0)) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_H18_31) && hbv_main.ATldv_blast_assert.split_K18_296 != hbv_main.ATldv_blast_assert.split_G18_436)) && !(hbv_main.ATldv_blast_assert.split_U5_447 != hbv_main.ATldv_blast_assert.split_W5_381[hbv_main.ATldv_blast_assert.split_X5_357] && hbv_main.ATldv_blast_assert.split_L6_106)) && !((hbv_main.ATldv_blast_assert.split_D20_35 && hbv_main.ATldv_blast_assert.split_T19_191) && hbv_main.ATldv_blast_assert.split_U19_190 != hbv_main.ATldv_blast_assert.split_B20_33)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && 0 < hbv_main.ATldv_blast_assert.split_L5_76) && hbv_main.ATldv_blast_assert.split_X3_178 <= 0)) && !((hbv_main.ATldv_blast_assert.split_L16_197 && hbv_main.ATldv_blast_assert.split_J16_443) && hbv_main.ATldv_blast_assert.split_X14_145)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_G2_216 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && !((hbv_main.ATldv_blast_assert.split_O13_266 != 4 && hbv_main.ATldv_blast_assert.split_K13_267 == 0) && hbv_main.ATldv_blast_assert.split_J1_27)) && !((hbv_main.ATldv_blast_assert.split_N5_105 <= 0 && hbv_main.ATldv_blast_assert.split_L6_106) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && hbv_main.ATldv_blast_assert.split_P1_497 == hbv_main.ATldv_blast_assert.split_N1_498) && hbv_main.ATldv_blast_assert.split_N19_220 == hbv_main.ATldv_blast_assert.split_C19_221) && hbv_main.ATldv_blast_assert.split_C7_459 == 32 + hbv_main.ATldv_blast_assert.split_D7_142) && !(hbv_main.ATldv_blast_assert.split_P9_369[hbv_main.ATldv_blast_assert.split_Q9_211 := hbv_main.ATldv_blast_assert.split_R9_370] != hbv_main.ATldv_blast_assert.split_U9_371 && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_T12_478 != hbv_main.ATldv_blast_assert.split_P12_13[hbv_main.ATldv_blast_assert.split_A12_395 := hbv_main.ATldv_blast_assert.split_B12_496] && hbv_main.ATldv_blast_assert.split_X12_204)) && !(hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_B13_12 <= 0)) && !(hbv_main.ATldv_blast_assert.split_L5_76 <= 0 && hbv_main.ATldv_blast_assert.split_H5_90)) && !(((hbv_main.ATldv_blast_assert.split_J1_27 && (!hbv_main.ATldv_blast_assert.split_J1_27 || !hbv_main.ATldv_blast_assert.split_B2_11)) && (!hbv_main.ATldv_blast_assert.split_X12_204 || !hbv_main.ATldv_blast_assert.split_J1_27)) && (!hbv_main.ATldv_blast_assert.split_J1_27 || !hbv_main.ATldv_blast_assert.split_M1_17))) && !((hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_D20_35) && hbv_main.ATldv_blast_assert.split_M19_444 != hbv_main.ATldv_blast_assert.split_B20_33)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_A2_121[hbv_main.ATldv_blast_assert.split_Z1_354] != hbv_main.ATldv_blast_assert.split_C2_123)) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_H18_31) && hbv_main.ATldv_blast_assert.split_J18_69 != hbv_main.ATldv_blast_assert.split_F18_393)) && !((hbv_main.ATldv_blast_assert.split_A7_53 && hbv_main.ATldv_blast_assert.split_X_307) && hbv_main.ATldv_blast_assert.split_D1_408 != hbv_main.ATldv_blast_assert.split_Y_518)) && !((hbv_main.ATldv_blast_assert.split_H19_380 != hbv_main.ATldv_blast_assert.split_N18_363 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_T18_119)) && !(hbv_main.ATldv_blast_assert.split_G12_78 && !hbv_main.ATldv_blast_assert.split_F12_79)) && !((hbv_main.ATldv_blast_assert.split_L15_323 && hbv_main.ATldv_blast_assert.split_Y13_352) && hbv_main.ATldv_blast_assert.split_D14_292 != hbv_main.ATldv_blast_assert.split_Z13_351)) && !((0 < hbv_main.ATldv_blast_assert.split_B11_222 && hbv_main.ATldv_blast_assert.split_C11_223 <= 0) && hbv_main.ATldv_blast_assert.split_O1_44)) && !(((!hbv_main.ATldv_blast_assert.split_A7_53 || !hbv_main.ATldv_blast_assert.split_X_307) && (!hbv_main.ATldv_blast_assert.split_B1_308 || !hbv_main.ATldv_blast_assert.split_A1_274)) && hbv_main.ATldv_blast_assert.split_A7_53)) && !((hbv_main.ATldv_blast_assert.split_W6_155 != hbv_main.ATldv_blast_assert.split_S6_137 && hbv_main.ATldv_blast_assert.split_R6_152) && hbv_main.ATldv_blast_assert.split_L7_238)) && !((hbv_main.ATldv_blast_assert.split_I18_328 != hbv_main.ATldv_blast_assert.split_Q_2 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_H18_31)) && !((hbv_main.ATldv_blast_assert.split_X7_234 != hbv_main.ATldv_blast_assert.split_M7_237 && hbv_main.ATldv_blast_assert.split_L7_238) && hbv_main.ATldv_blast_assert.split_C8_239)) && !((!hbv_main.ATldv_blast_assert.split_M12_338 || 3 != hbv_main.ATldv_blast_assert.split_E12_339) && (3 == hbv_main.ATldv_blast_assert.split_E12_339 || hbv_main.ATldv_blast_assert.split_M12_338))) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_D18_150) && hbv_main.ATldv_blast_assert.split_E18_84 != hbv_main.ATldv_blast_assert.split_Q_2)) && !((hbv_main.ATldv_blast_assert.split_K18_296 != hbv_main.ATldv_blast_assert.split_U17_297 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_V17_112)) && !((hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_D19_391 != hbv_main.ATldv_blast_assert.split_A8_474)) && !((hbv_main.ATldv_blast_assert.split_B2_122 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_C_56)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_L3_342 == 0) && 1073741952 != hbv_main.ATldv_blast_assert.split_V3_98)) && !(hbv_main.ATldv_blast_assert.split_U9_371[hbv_main.ATldv_blast_assert.split_V9_157 := hbv_main.ATldv_blast_assert.split_W9_471] != hbv_main.ATldv_blast_assert.split_X9_472 && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_D10_341[hbv_main.ATldv_blast_assert.split_E10_309 := hbv_main.ATldv_blast_assert.split_F10_523] != hbv_main.ATldv_blast_assert.split_I10_332 && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_M16_187) && !((!hbv_main.ATldv_blast_assert.split_O1_44 || !hbv_main.ATldv_blast_assert.split_X14_145) && hbv_main.ATldv_blast_assert.split_O1_44)) && !((hbv_main.ATldv_blast_assert.split_V15_188 != hbv_main.ATldv_blast_assert.split_U15_489 && hbv_main.ATldv_blast_assert.split_S_5) && hbv_main.ATldv_blast_assert.split_C1_6)) && !(hbv_main.ATldv_blast_assert.split_X14_145 && hbv_main.ATldv_blast_assert.split_H17_28[hbv_main.ATldv_blast_assert.split_V14_250 := hbv_main.ATldv_blast_assert.split_N8_442] != hbv_main.ATldv_blast_assert.split_B15_451)) && !(hbv_main.ATldv_blast_assert.split_F14_26 && hbv_main.ATldv_blast_assert.split_U13_202 != hbv_main.ATldv_blast_assert.split_E15_149[hbv_main.ATldv_blast_assert.split_T13_25])) && !((hbv_main.ATldv_blast_assert.split_V18_161 && hbv_main.ATldv_blast_assert.split_T18_119) && hbv_main.ATldv_blast_assert.split_Z19_247)) && hbv_main.ATldv_blast_assert.split_M8_426 == hbv_main.ATldv_blast_assert.split_L8_302 + 1) && hbv_main.ATldv_blast_assert.split_R13_24 == hbv_main.ATldv_blast_assert.split_E1_37) && !((hbv_main.ATldv_blast_assert.split_C13_199 != hbv_main.ATldv_blast_assert.split_W12_300 && hbv_main.ATldv_blast_assert.split_J1_27) && hbv_main.ATldv_blast_assert.split_B2_11)) && hbv_main.ATldv_blast_assert.split_Y_518 == hbv_main.ATldv_blast_assert.split_U_480) && !(hbv_main.ATldv_blast_assert.split_T19_191 && hbv_main.ATldv_blast_assert.split_Y18_279)) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_T18_119) && hbv_main.ATldv_blast_assert.split_I19_118 != hbv_main.ATldv_blast_assert.split_X_1)) && !(hbv_main.ATldv_blast_assert.split_L5_76 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52)) && hbv_main.ATldv_blast_assert.split_G19_362 == hbv_main.ATldv_blast_assert.split_W19_376) && hbv_main.ATldv_blast_assert.split_V6_154 == hbv_main.ATldv_blast_assert.split_Q6_483) && !((hbv_main.ATldv_blast_assert.split_H12_203 || 5 == hbv_main.ATldv_blast_assert.split_E12_339) && (!hbv_main.ATldv_blast_assert.split_H12_203 || 5 != hbv_main.ATldv_blast_assert.split_E12_339))) && hbv_main.ATldv_blast_assert.split_E18_84 == hbv_main.ATldv_blast_assert.split_L17_85) && !(hbv_main.ATldv_blast_assert.split_X12_204 && hbv_main.ATldv_blast_assert.split_B13_12 <= 0)) && !((hbv_main.ATldv_blast_assert.split_L12_81 && hbv_main.ATldv_blast_assert.split_M1_17) && !hbv_main.ATldv_blast_assert.split_M12_338)) && hbv_main.ATldv_blast_assert.split_O10_68 == hbv_main.ATldv_blast_assert.split_M_509) && !((hbv_main.ATldv_blast_assert.split_M4_208 && hbv_main.ATldv_blast_assert.split_N4_209) && hbv_main.ATldv_blast_assert.split_P4_91)) && !(hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_Q5_326 != hbv_main.ATldv_blast_assert.split_R5_280[hbv_main.ATldv_blast_assert.split_B6_382])) && hbv_main.ATldv_blast_assert.split_B13_12 + 168 == hbv_main.ATldv_blast_assert.split_Q12_14) && hbv_main.ATldv_blast_assert.split_I6_306 == hbv_main.ATldv_blast_assert.split_B19_299) && !(hbv_main.ATldv_blast_assert.split_P15_113 && (!hbv_main.ATldv_blast_assert.split_F14_26 || !hbv_main.ATldv_blast_assert.split_P15_113))) && hbv_main.ATldv_blast_assert.split_O17_130 == hbv_main.ATldv_blast_assert.split_F1_74) && !(hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_M13_36 != hbv_main.ATldv_blast_assert.split_H13_201[hbv_main.ATldv_blast_assert.split_I13_87 := hbv_main.ATldv_blast_assert.split_J13_415])) && hbv_main.ATldv_blast_assert.split_U3_97 == 88 + hbv_main.ATldv_blast_assert.split_L5_76) && !((hbv_main.ATldv_blast_assert.split_S9_171 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_W11_146)) && hbv_main.ATldv_blast_assert.split_C1_424 == 0) && !((!hbv_main.ATldv_blast_assert.split_S14_397 || hbv_main.ATldv_blast_assert.split_R14_398 != 0) && (hbv_main.ATldv_blast_assert.split_R14_398 == 0 || hbv_main.ATldv_blast_assert.split_S14_397))) && 16 + hbv_main.ATldv_blast_assert.split_R10_366 == hbv_main.ATldv_blast_assert.split_S10_367) && !(hbv_main.ATldv_blast_assert.split_M1_17 && (!hbv_main.ATldv_blast_assert.split_L12_81 || !hbv_main.ATldv_blast_assert.split_M1_17))) && !(hbv_main.ATldv_blast_assert.split_K16_46 <= 0 && hbv_main.ATldv_blast_assert.split_J1_27)) && !((!hbv_main.ATldv_blast_assert.split_O14_170 || !hbv_main.ATldv_blast_assert.split_W16_136) && hbv_main.ATldv_blast_assert.split_W16_136)) && hbv_main.ATldv_blast_assert.split_Z13_351 == hbv_main.ATldv_blast_assert.split_V13_514) && !((hbv_main.ATldv_blast_assert.split_S_5 && hbv_main.ATldv_blast_assert.split_C1_6) && hbv_main.ATldv_blast_assert.split_S15_231 != hbv_main.ATldv_blast_assert.split_L17_85)) && !((hbv_main.ATldv_blast_assert.split_J1_27 && hbv_main.ATldv_blast_assert.split_D13_200 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && !(hbv_main.ATldv_blast_assert.split_D7_142 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_S18_403 && (!hbv_main.ATldv_blast_assert.split_Z19_247 || !hbv_main.ATldv_blast_assert.split_S18_403))) && hbv_main.ATldv_blast_assert.split_T_159 == hbv_main.ATldv_blast_assert.split_S_160) && hbv_main.ATldv_blast_assert.split_G16_304 + 1 == hbv_main.ATldv_blast_assert.split_F16_165) && !((hbv_main.ATldv_blast_assert.split_F17_179 != hbv_main.ATldv_blast_assert.split_A17_180 && hbv_main.ATldv_blast_assert.split_C17_181) && hbv_main.ATldv_blast_assert.split_B17_182)) && !((hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_D6_453 != hbv_main.ATldv_blast_assert.split_A19_476)) && hbv_main.ATldv_blast_assert.split_S6_137 == hbv_main.ATldv_blast_assert.split_O6_138) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_O_40 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_G4_177)) && !(0 < hbv_main.ATldv_blast_assert.split_G8_392 && !hbv_main.ATldv_blast_assert.split_H8_449)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_L11_57 != hbv_main.ATldv_blast_assert.split_I11_117[hbv_main.ATldv_blast_assert.split_J11_485 := hbv_main.ATldv_blast_assert.split_K11_486])) && hbv_main.ATldv_blast_assert.split_K17_139 == hbv_main.ATldv_blast_assert.split_X15_140) && !((hbv_main.ATldv_blast_assert.split_K16_46 == 0 || hbv_main.ATldv_blast_assert.split_J_405) && (!hbv_main.ATldv_blast_assert.split_J_405 || hbv_main.ATldv_blast_assert.split_K16_46 != 0))) && !((hbv_main.ATldv_blast_assert.split_K12_513 <= 0 && hbv_main.ATldv_blast_assert.split_B2_11) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && 40 + hbv_main.ATldv_blast_assert.split_D7_142 == hbv_main.ATldv_blast_assert.split_V1_240) && hbv_main.ATldv_blast_assert.split_M18_361 == hbv_main.ATldv_blast_assert.split_J18_69) && !((hbv_main.ATldv_blast_assert.split_V4_207 && hbv_main.ATldv_blast_assert.split_M4_208) && !hbv_main.ATldv_blast_assert.split_N4_209)) && !((hbv_main.ATldv_blast_assert.split_A5_243 <= 0 && hbv_main.ATldv_blast_assert.split_J5_224) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && hbv_main.ATldv_blast_assert.split_N17_132 == hbv_main.ATldv_blast_assert.split_A17_180) && hbv_main.ATldv_blast_assert.split_Q6_483 == hbv_main.ATldv_blast_assert.split_I7_158) && hbv_main.ATldv_blast_assert.split_G18_436 == hbv_main.ATldv_blast_assert.split_N17_132) && 1122 + hbv_main.ATldv_blast_assert.split_W11_146 == hbv_main.ATldv_blast_assert.split_N9_192) && !((hbv_main.ATldv_blast_assert.split_Q4_214 && hbv_main.ATldv_blast_assert.split_R4_215) && hbv_main.ATldv_blast_assert.split_P4_91)) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_R17_396) && hbv_main.ATldv_blast_assert.split_P17_217 != hbv_main.ATldv_blast_assert.split_J18_69)) && !(hbv_main.ATldv_blast_assert.split_P10_434 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44)) && !((3 == hbv_main.ATldv_blast_assert.split_O4_196 || hbv_main.ATldv_blast_assert.split_W4_411) && (!hbv_main.ATldv_blast_assert.split_W4_411 || 3 != hbv_main.ATldv_blast_assert.split_O4_196))) && !((!hbv_main.ATldv_blast_assert.split_T4_213 || !hbv_main.ATldv_blast_assert.split_F5_77) && hbv_main.ATldv_blast_assert.split_F5_77)) && !(hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_K6_288)) && hbv_main.ATldv_blast_assert.split_L1_18 == hbv_main.ATldv_blast_assert.split_Z1_19) && !(hbv_main.ATldv_blast_assert.split_H_314 && (!hbv_main.ATldv_blast_assert.split_F_315 || !hbv_main.ATldv_blast_assert.split_H_314))) && !((hbv_main.ATldv_blast_assert.split_V17_112 && hbv_main.ATldv_blast_assert.split_D_389) && !hbv_main.ATldv_blast_assert.split_E_425)) && !(hbv_main.ATldv_blast_assert.split_T1_420 != hbv_main.ATldv_blast_assert.split_Q1_418[hbv_main.ATldv_blast_assert.split_R1_92 := hbv_main.ATldv_blast_assert.split_S1_419] && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_D_389 && (!hbv_main.ATldv_blast_assert.split_F_315 || !hbv_main.ATldv_blast_assert.split_D_389))) && !(!hbv_main.ATldv_blast_assert.split_W13_345 && 0 < hbv_main.ATldv_blast_assert.split_X13_346)) && hbv_main.ATldv_blast_assert.split_E1_37 == hbv_main.ATldv_blast_assert.split_Z_49) && !((hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_E8_319 != hbv_main.ATldv_blast_assert.split_D8_290)) && !((hbv_main.ATldv_blast_assert.split_F14_26 && hbv_main.ATldv_blast_assert.split_I14_416) && hbv_main.ATldv_blast_assert.split_J1_27)) && !((hbv_main.ATldv_blast_assert.split_G15_7 != hbv_main.ATldv_blast_assert.split_S13_336 && hbv_main.ATldv_blast_assert.split_F14_26) && hbv_main.ATldv_blast_assert.split_J1_27)) && hbv_main.ATldv_blast_assert.split_H1_141 == hbv_main.ATldv_blast_assert.split_B6_382) && !(hbv_main.ATldv_blast_assert.split_G13_86 <= 0 && hbv_main.ATldv_blast_assert.split_J1_27)) && !(hbv_main.ATldv_blast_assert.split_I10_332[hbv_main.ATldv_blast_assert.split_J10_333 := hbv_main.ATldv_blast_assert.split_K10_355] != hbv_main.ATldv_blast_assert.split_H10_508 && hbv_main.ATldv_blast_assert.split_O1_44)) && 30 + hbv_main.ATldv_blast_assert.split_O10_68 == hbv_main.ATldv_blast_assert.split_V9_157) && hbv_main.ATldv_blast_assert.split_N6_259 == hbv_main.ATldv_blast_assert.split_F6_260) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_C2_48 != hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_G3_406])) && !((hbv_main.ATldv_blast_assert.split_U11_95 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && 40 + hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_F9_456) && hbv_main.ATldv_blast_assert.split_O17_130 == hbv_main.ATldv_blast_assert.split_S7_131) && hbv_main.ATldv_blast_assert.split_I2_287 == hbv_main.ATldv_blast_assert.split_G4_177 + 1124) && !((hbv_main.ATldv_blast_assert.split_P16_350 || (hbv_main.ATldv_blast_assert.split_S14_397 && hbv_main.ATldv_blast_assert.split_T14_183)) && ((!hbv_main.ATldv_blast_assert.split_T14_183 || !hbv_main.ATldv_blast_assert.split_P16_350) || !hbv_main.ATldv_blast_assert.split_S14_397))) && !(hbv_main.ATldv_blast_assert.split_L5_76 <= 0 && hbv_main.ATldv_blast_assert.split_F5_77)) && 560 + hbv_main.ATldv_blast_assert.split_C_56 == hbv_main.ATldv_blast_assert.split_S2_242) && !(hbv_main.ATldv_blast_assert.split_B11_222 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_Y7_262 != hbv_main.ATldv_blast_assert.split_V7_261[hbv_main.ATldv_blast_assert.split_T7_255] && hbv_main.ATldv_blast_assert.split_C8_239)) && hbv_main.ATldv_blast_assert.split_U1_517 == hbv_main.ATldv_blast_assert.split_C_56 + 8) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_A11_520 == 0) && 1073741952 != hbv_main.ATldv_blast_assert.split_K11_486)) && !((hbv_main.ATldv_blast_assert.split_L15_323 && hbv_main.ATldv_blast_assert.split_S_5) && hbv_main.ATldv_blast_assert.split_K15_484 != hbv_main.ATldv_blast_assert.split_L17_85)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_F4_490 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_G4_177)) && hbv_main.ATldv_blast_assert.split_Q7_156 == hbv_main.ATldv_blast_assert.split_J7_22) && hbv_main.ATldv_blast_assert.split_F17_179 == hbv_main.ATldv_blast_assert.split_Q17_464) && !(hbv_main.ATldv_blast_assert.split_K2_318 != hbv_main.ATldv_blast_assert.split_F2_124[hbv_main.ATldv_blast_assert.split_G2_216 := hbv_main.ATldv_blast_assert.split_H2_317] && hbv_main.ATldv_blast_assert.split_I4_52)) && !((hbv_main.ATldv_blast_assert.split_F16_165 != hbv_main.ATldv_blast_assert.split_B16_448 && hbv_main.ATldv_blast_assert.split_Z17_72) && hbv_main.ATldv_blast_assert.split_A16_291)) && hbv_main.ATldv_blast_assert.split_Z_49 == hbv_main.ATldv_blast_assert.split_R8_452) && hbv_main.ATldv_blast_assert.split_W2_227 == 40 + hbv_main.ATldv_blast_assert.split_C_56) && hbv_main.ATldv_blast_assert.split_Q16_185 == hbv_main.ATldv_blast_assert.split_U16_186) && !((hbv_main.ATldv_blast_assert.split_C1_424 != hbv_main.ATldv_blast_assert.split_D1_408 && hbv_main.ATldv_blast_assert.split_A1_274) && hbv_main.ATldv_blast_assert.split_B1_308)) && !((hbv_main.ATldv_blast_assert.split_H9_42 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && !((hbv_main.ATldv_blast_assert.split_J19_162 != hbv_main.ATldv_blast_assert.split_V19_163 && hbv_main.ATldv_blast_assert.split_L19_109) && hbv_main.ATldv_blast_assert.split_D20_35)) && !((hbv_main.ATldv_blast_assert.split_Y6_102 && hbv_main.ATldv_blast_assert.split_O7_103) && !hbv_main.ATldv_blast_assert.split_Z6_104)) && !((hbv_main.ATldv_blast_assert.split_M1_17 && 0 < hbv_main.ATldv_blast_assert.split_B13_12) && hbv_main.ATldv_blast_assert.split_Q12_14 <= 0)) && !((hbv_main.ATldv_blast_assert.split_B10_126 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && hbv_main.ATldv_blast_assert.split_X3_178 == 104 + hbv_main.ATldv_blast_assert.split_L5_76) && !((hbv_main.ATldv_blast_assert.split_U3_97 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && !(hbv_main.ATldv_blast_assert.split_Y13_352 && (!hbv_main.ATldv_blast_assert.split_A14_295 || !hbv_main.ATldv_blast_assert.split_Y13_352))) && !(((!hbv_main.ATldv_blast_assert.split_J_405 && !hbv_main.ATldv_blast_assert.split_K_423) || !hbv_main.ATldv_blast_assert.split_T16_210) && ((hbv_main.ATldv_blast_assert.split_T16_210 || hbv_main.ATldv_blast_assert.split_J_405) || hbv_main.ATldv_blast_assert.split_K_423))) && !(hbv_main.ATldv_blast_assert.split_P4_91 && (!hbv_main.ATldv_blast_assert.split_P4_91 || !hbv_main.ATldv_blast_assert.split_M4_208))) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_E9_283 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && hbv_main.ATldv_blast_assert.split_O5_198 == hbv_main.ATldv_blast_assert.split_D7_142 + 8) && !((!hbv_main.ATldv_blast_assert.split_B17_182 || !hbv_main.ATldv_blast_assert.split_L16_197) && hbv_main.ATldv_blast_assert.split_L16_197)) && 6 + hbv_main.ATldv_blast_assert.split_B11_222 == hbv_main.ATldv_blast_assert.split_C11_223) && !((hbv_main.ATldv_blast_assert.split_D16_167 && hbv_main.ATldv_blast_assert.split_C16_168) && hbv_main.ATldv_blast_assert.split_F16_165 != hbv_main.ATldv_blast_assert.split_E16_166)) && !((hbv_main.ATldv_blast_assert.split_R15_3 != hbv_main.ATldv_blast_assert.split_J17_4 && hbv_main.ATldv_blast_assert.split_S_5) && hbv_main.ATldv_blast_assert.split_C1_6)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_K10_355 != 10) && hbv_main.ATldv_blast_assert.split_G10_334 == 0)) && !((hbv_main.ATldv_blast_assert.split_D7_142 != hbv_main.ATldv_blast_assert.split_N_465 && hbv_main.ATldv_blast_assert.split_J8_273) && hbv_main.ATldv_blast_assert.split_A1_274)) && hbv_main.ATldv_blast_assert.split_L5_76 + 132 == hbv_main.ATldv_blast_assert.split_A4_470) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_S10_367] != hbv_main.ATldv_blast_assert.split_B11_222)) && !((hbv_main.ATldv_blast_assert.split_P15_113 && hbv_main.ATldv_blast_assert.split_S_5) && hbv_main.ATldv_blast_assert.split_O15_331 != hbv_main.ATldv_blast_assert.split_L17_85)) && !((((!hbv_main.ATldv_blast_assert.split_L6_106 || !hbv_main.ATldv_blast_assert.split_J5_224) && (!hbv_main.ATldv_blast_assert.split_L6_106 || !hbv_main.ATldv_blast_assert.split_H5_90)) && (!hbv_main.ATldv_blast_assert.split_L6_106 || !hbv_main.ATldv_blast_assert.split_F5_77)) && hbv_main.ATldv_blast_assert.split_L6_106)) && hbv_main.ATldv_blast_assert.split_I9_241 == hbv_main.ATldv_blast_assert.split_J9_348) && !(hbv_main.ATldv_blast_assert.split_W11_146 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_D4_446[hbv_main.ATldv_blast_assert.split_E4_120 := hbv_main.ATldv_blast_assert.split_D7_142] != hbv_main.ATldv_blast_assert.split_Z4_194)) && hbv_main.ATldv_blast_assert.split_V_38 + 100 == hbv_main.ATldv_blast_assert.split_N13_322) && hbv_main.ATldv_blast_assert.split_X4_65 + 1 == hbv_main.ATldv_blast_assert.split_Y4_66) && !((hbv_main.ATldv_blast_assert.split_J8_273 && 0 < hbv_main.ATldv_blast_assert.split_W11_146) && hbv_main.ATldv_blast_assert.split_H11_116 <= 0)) && !((hbv_main.ATldv_blast_assert.split_J8_273 && hbv_main.ATldv_blast_assert.split_K8_360) && hbv_main.ATldv_blast_assert.split_A1_274)) && !((hbv_main.ATldv_blast_assert.split_C17_181 && hbv_main.ATldv_blast_assert.split_B17_182) && hbv_main.ATldv_blast_assert.split_G17_374 != hbv_main.ATldv_blast_assert.split_D17_375)) && !(hbv_main.ATldv_blast_assert.split_C12_432 && (!hbv_main.ATldv_blast_assert.split_C12_432 || !hbv_main.ATldv_blast_assert.split_O1_44))) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_Y3_256 != hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_T7_255])) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_D4_446 != hbv_main.ATldv_blast_assert.split_B4_505[hbv_main.ATldv_blast_assert.split_C4_460 := hbv_main.ATldv_blast_assert.split_S11_63])) && !((hbv_main.ATldv_blast_assert.split_K4_257 <= 0 && hbv_main.ATldv_blast_assert.split_H5_90) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && hbv_main.ATldv_blast_assert.split_X10_229 == hbv_main.ATldv_blast_assert.split_U10_249) && !(((!hbv_main.ATldv_blast_assert.split_X16_135 || !hbv_main.ATldv_blast_assert.split_W16_136) && (!hbv_main.ATldv_blast_assert.split_B17_182 || !hbv_main.ATldv_blast_assert.split_C17_181)) && hbv_main.ATldv_blast_assert.split_R17_396)) && !((hbv_main.ATldv_blast_assert.split_A1_274 && hbv_main.ATldv_blast_assert.split_B1_308) && hbv_main.ATldv_blast_assert.split_W7_324 != hbv_main.ATldv_blast_assert.split_Z_373)) && !((!hbv_main.ATldv_blast_assert.split_V18_161 || hbv_main.ATldv_blast_assert.split_R18_368 != 0) && (hbv_main.ATldv_blast_assert.split_R18_368 == 0 || hbv_main.ATldv_blast_assert.split_V18_161))) && hbv_main.ATldv_blast_assert.split_M1_429 == hbv_main.ATldv_blast_assert.split_K1_430) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_Z_49 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_K16_46)) && !((!hbv_main.ATldv_blast_assert.split_G_313 && hbv_main.ATldv_blast_assert.split_H_314) && hbv_main.ATldv_blast_assert.split_F_315)) && !((hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_L6_106) && hbv_main.ATldv_blast_assert.split_C6_390 != hbv_main.ATldv_blast_assert.split_Z18_244)) && !((hbv_main.ATldv_blast_assert.split_W19_376 != hbv_main.ATldv_blast_assert.split_V19_163 && hbv_main.ATldv_blast_assert.split_Z19_247) && hbv_main.ATldv_blast_assert.split_A20_248)) && hbv_main.ATldv_blast_assert.split_W7_324 == hbv_main.ATldv_blast_assert.split_A8_474) && !((hbv_main.ATldv_blast_assert.split_A7_53 && hbv_main.ATldv_blast_assert.split_X_307) && hbv_main.ATldv_blast_assert.split_W7_324 != hbv_main.ATldv_blast_assert.split_W_325)) && hbv_main.ATldv_blast_assert.split_X10_229 * 32768 == hbv_main.ATldv_blast_assert.split_Z10_230) && !(hbv_main.ATldv_blast_assert.split_R7_23 && hbv_main.ATldv_blast_assert.split_E7_20[hbv_main.ATldv_blast_assert.split_J_21 := 0] != hbv_main.ATldv_blast_assert.split_J7_22)) && !((hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_E19_479 != hbv_main.ATldv_blast_assert.split_B8_235)) && hbv_main.ATldv_blast_assert.split_N5_105 == 160 + hbv_main.ATldv_blast_assert.split_L5_76) && !(hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_Q10_394] != hbv_main.ATldv_blast_assert.split_C3_172 && hbv_main.ATldv_blast_assert.split_I4_52)) && !(!hbv_main.ATldv_blast_assert.split_Z19_247 && hbv_main.ATldv_blast_assert.split_A20_248)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_M3_175 != hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_D3_173])) && !((!hbv_main.ATldv_blast_assert.split_A7_53 || !hbv_main.ATldv_blast_assert.split_R7_23) && hbv_main.ATldv_blast_assert.split_R7_23)) && hbv_main.ATldv_blast_assert.split_U11_95 == 176 + hbv_main.ATldv_blast_assert.split_B13_12) && !((!hbv_main.ATldv_blast_assert.split_D_389 || !hbv_main.ATldv_blast_assert.split_V17_112) && hbv_main.ATldv_blast_assert.split_V17_112)) && !((hbv_main.ATldv_blast_assert.split_L16_197 && hbv_main.ATldv_blast_assert.split_T16_210) && hbv_main.ATldv_blast_assert.split_B17_182)) && !((hbv_main.ATldv_blast_assert.split_S17_441 != hbv_main.ATldv_blast_assert.split_Q_2 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_R17_396)) && hbv_main.ATldv_blast_assert.split_W7_324 == hbv_main.ATldv_blast_assert.split_D6_453) && !((((!hbv_main.ATldv_blast_assert.split_S_5 || !hbv_main.ATldv_blast_assert.split_P15_113) && hbv_main.ATldv_blast_assert.split_S_5) && (!hbv_main.ATldv_blast_assert.split_S_5 || !hbv_main.ATldv_blast_assert.split_L15_323)) && (!hbv_main.ATldv_blast_assert.split_S_5 || !hbv_main.ATldv_blast_assert.split_C1_6))) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_K9_43[hbv_main.ATldv_blast_assert.split_L9_410 := hbv_main.ATldv_blast_assert.split_M9_349] != hbv_main.ATldv_blast_assert.split_P9_369)) && 16 + hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_W8_107) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_E7_20[hbv_main.ATldv_blast_assert.split_I1_493 := hbv_main.ATldv_blast_assert.split_J1_494] != hbv_main.ATldv_blast_assert.split_L1_495)) && !(hbv_main.ATldv_blast_assert.split_L19_109 && hbv_main.ATldv_blast_assert.split_H6_110)) && !(hbv_main.ATldv_blast_assert.split_V5_356 <= 0 && hbv_main.ATldv_blast_assert.split_L6_106)) && hbv_main.ATldv_blast_assert.split_J_21 == hbv_main.ATldv_blast_assert.split_C7_459) && !((hbv_main.ATldv_blast_assert.split_Q15_151 != hbv_main.ATldv_blast_assert.split_V15_188 && hbv_main.ATldv_blast_assert.split_P15_113) && hbv_main.ATldv_blast_assert.split_S_5)) && !(!hbv_main.ATldv_blast_assert.split_T18_119 && hbv_main.ATldv_blast_assert.split_U18_134)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_P11_388 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_B13_12)) && !((hbv_main.ATldv_blast_assert.split_L1_18 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && hbv_main.ATldv_blast_assert.split_V1_47 == 256 * hbv_main.ATldv_blast_assert.split_C2_48) && hbv_main.ATldv_blast_assert.split_F15_100 == hbv_main.ATldv_blast_assert.split_N14_101) && hbv_main.ATldv_blast_assert.split_O9_516 == hbv_main.ATldv_blast_assert.split_N9_192) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_V17_112) && hbv_main.ATldv_blast_assert.split_Q_2 != hbv_main.ATldv_blast_assert.split_W17_353)) && hbv_main.ATldv_blast_assert.split_K15_484 == hbv_main.ATldv_blast_assert.split_D15_285) && !(hbv_main.ATldv_blast_assert.split_K16_46 <= 0 && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_Y2_347 == hbv_main.ATldv_blast_assert.split_A3_233) && hbv_main.ATldv_blast_assert.split_I15_329 == hbv_main.ATldv_blast_assert.split_U15_489) && hbv_main.ATldv_blast_assert.split_W11_146 == hbv_main.ATldv_blast_assert.split_P_147) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_M3_175 <= 0)) && !(hbv_main.ATldv_blast_assert.split_U7_524 && hbv_main.ATldv_blast_assert.split_C8_239)) && !((!hbv_main.ATldv_blast_assert.split_B17_182 || !hbv_main.ATldv_blast_assert.split_J8_273) && hbv_main.ATldv_blast_assert.split_B17_182)) && hbv_main.ATldv_blast_assert.split_K17_139 == hbv_main.ATldv_blast_assert.split_Z15_301) && !(hbv_main.ATldv_blast_assert.split_R2_278 != hbv_main.ATldv_blast_assert.split_P2_275[hbv_main.ATldv_blast_assert.split_Q2_276 := hbv_main.ATldv_blast_assert.split_C10_277] && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_B2_11 && hbv_main.ATldv_blast_assert.split_P12_13[hbv_main.ATldv_blast_assert.split_K12_513 := hbv_main.ATldv_blast_assert.split_O12_9] != hbv_main.ATldv_blast_assert.split_S12_502)) && !((0 < hbv_main.ATldv_blast_assert.split_R10_366 && hbv_main.ATldv_blast_assert.split_S10_367 <= 0) && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_N17_132 == hbv_main.ATldv_blast_assert.split_Z_373) && 108 + hbv_main.ATldv_blast_assert.split_F4_490 == hbv_main.ATldv_blast_assert.split_G4_177) && !((0 < hbv_main.ATldv_blast_assert.split_D7_142 && hbv_main.ATldv_blast_assert.split_I4_52) && hbv_main.ATldv_blast_assert.split_V1_240 <= 0)) && !(hbv_main.ATldv_blast_assert.split_O7_103 && (!hbv_main.ATldv_blast_assert.split_Y6_102 || !hbv_main.ATldv_blast_assert.split_O7_103))) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_O11_60[hbv_main.ATldv_blast_assert.split_P11_388 := 8] != hbv_main.ATldv_blast_assert.split_Q11_61)) && hbv_main.ATldv_blast_assert.split_O10_68 + 8 == hbv_main.ATldv_blast_assert.split_E9_283) && !((hbv_main.ATldv_blast_assert.split_W13_345 && hbv_main.ATldv_blast_assert.split_Y13_352) && hbv_main.ATldv_blast_assert.split_A14_295)) && !(hbv_main.ATldv_blast_assert.split_X12_204 && (!hbv_main.ATldv_blast_assert.split_X12_204 || !hbv_main.ATldv_blast_assert.split_F12_79))) && !((hbv_main.ATldv_blast_assert.split_O1_44 && 0 < hbv_main.ATldv_blast_assert.split_W11_146) && hbv_main.ATldv_blast_assert.split_N9_192 <= 0)) && !((hbv_main.ATldv_blast_assert.split_E8_319 == 0 || hbv_main.ATldv_blast_assert.split_F8_320) && (hbv_main.ATldv_blast_assert.split_E8_319 != 0 || !hbv_main.ATldv_blast_assert.split_F8_320))) && !((hbv_main.ATldv_blast_assert.split_C4_460 <= 0 && hbv_main.ATldv_blast_assert.split_I4_52) && 0 < hbv_main.ATldv_blast_assert.split_L5_76)) && hbv_main.ATldv_blast_assert.split_X15_140 == hbv_main.ATldv_blast_assert.split_B16_448) && !((hbv_main.ATldv_blast_assert.split_I4_52 && 0 < hbv_main.ATldv_blast_assert.split_G4_177) && hbv_main.ATldv_blast_assert.split_I2_287 <= 0)) && 176 + hbv_main.ATldv_blast_assert.split_L5_76 == hbv_main.ATldv_blast_assert.split_E4_120) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_R3_427 := hbv_main.ATldv_blast_assert.split_S3_271] != hbv_main.ATldv_blast_assert.split_T3_96)) && !(hbv_main.ATldv_blast_assert.split_W13_345 && hbv_main.ATldv_blast_assert.split_X13_346 <= 0)) && hbv_main.ATldv_blast_assert.split_G1_73 == hbv_main.ATldv_blast_assert.split_F1_74 + 1) && !((hbv_main.ATldv_blast_assert.split_P4_91 && hbv_main.ATldv_blast_assert.split_H5_90) && !hbv_main.ATldv_blast_assert.split_R4_215)) && !((hbv_main.ATldv_blast_assert.split_C_522 == 0 || hbv_main.ATldv_blast_assert.split_E_425) && (hbv_main.ATldv_blast_assert.split_C_522 != 0 || !hbv_main.ATldv_blast_assert.split_E_425))) && !((hbv_main.ATldv_blast_assert.split_R19_488 != hbv_main.ATldv_blast_assert.split_V19_163 && hbv_main.ATldv_blast_assert.split_D20_35) && hbv_main.ATldv_blast_assert.split_T19_191)) && !(hbv_main.ATldv_blast_assert.split_L12_81 && (!hbv_main.ATldv_blast_assert.split_C12_432 || !hbv_main.ATldv_blast_assert.split_L12_81))) && !(hbv_main.ATldv_blast_assert.split_T11_64[hbv_main.ATldv_blast_assert.split_U11_95 := hbv_main.ATldv_blast_assert.split_K16_46] != hbv_main.ATldv_blast_assert.split_P12_13 && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_K16_46 + 8 == hbv_main.ATldv_blast_assert.split_E13_402) && hbv_main.ATldv_blast_assert.split_B_55 == 840 + hbv_main.ATldv_blast_assert.split_C_56) && !((!hbv_main.ATldv_blast_assert.split_V4_207 || !hbv_main.ATldv_blast_assert.split_J5_224) && hbv_main.ATldv_blast_assert.split_J5_224)) && hbv_main.ATldv_blast_assert.split_M17_30 == hbv_main.ATldv_blast_assert.split_F18_393) && hbv_main.ATldv_blast_assert.split_I17_303 == hbv_main.ATldv_blast_assert.split_G16_304) && !((hbv_main.ATldv_blast_assert.split_N8_442 != 0 || !hbv_main.ATldv_blast_assert.split_J16_443) && (hbv_main.ATldv_blast_assert.split_J16_443 || hbv_main.ATldv_blast_assert.split_N8_442 == 0))) && hbv_main.ATldv_blast_assert.split_X6_379 == hbv_main.ATldv_blast_assert.split_G7_251) && hbv_main.ATldv_blast_assert.split_O5_198 == hbv_main.ATldv_blast_assert.split_P5_281) && !((0 < hbv_main.ATldv_blast_assert.split_A15_83 && hbv_main.ATldv_blast_assert.split_Z14_504 <= 0) && hbv_main.ATldv_blast_assert.split_C1_6)) && !((hbv_main.ATldv_blast_assert.split_I4_52 && 0 < hbv_main.ATldv_blast_assert.split_L5_76) && hbv_main.ATldv_blast_assert.split_A4_470 <= 0)) && 552 + hbv_main.ATldv_blast_assert.split_O10_68 == hbv_main.ATldv_blast_assert.split_B10_126) && !(hbv_main.ATldv_blast_assert.split_O3_321 != hbv_main.ATldv_blast_assert.split_Q3_254[hbv_main.ATldv_blast_assert.split_N3_174] && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_M4_208 && (!hbv_main.ATldv_blast_assert.split_I4_52 || !hbv_main.ATldv_blast_assert.split_M4_208))) && !((!hbv_main.ATldv_blast_assert.split_D12_487 && hbv_main.ATldv_blast_assert.split_L12_81) && hbv_main.ATldv_blast_assert.split_C12_432)) && !((hbv_main.ATldv_blast_assert.split_C20_457 != hbv_main.ATldv_blast_assert.split_B20_33 && hbv_main.ATldv_blast_assert.split_Z19_247) && hbv_main.ATldv_blast_assert.split_A20_248)) && !((hbv_main.ATldv_blast_assert.split_O18_71 && hbv_main.ATldv_blast_assert.split_Z17_72) && hbv_main.ATldv_blast_assert.split_Q_2 != hbv_main.ATldv_blast_assert.split_A18_428)) && !(hbv_main.ATldv_blast_assert.split_O1_515[hbv_main.ATldv_blast_assert.split_P1_497 := hbv_main.ATldv_blast_assert.split_C_56] != hbv_main.ATldv_blast_assert.split_Q1_418 && hbv_main.ATldv_blast_assert.split_I4_52)) && !(hbv_main.ATldv_blast_assert.split_H5_90 && (!hbv_main.ATldv_blast_assert.split_H5_90 || !hbv_main.ATldv_blast_assert.split_P4_91))) && !((0 < hbv_main.ATldv_blast_assert.split_D7_142 && hbv_main.ATldv_blast_assert.split_I4_52) && hbv_main.ATldv_blast_assert.split_H1_141 <= 0)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_C_56 <= 0)) && !(hbv_main.ATldv_blast_assert.split_Q4_214 && !hbv_main.ATldv_blast_assert.split_P4_91)) && 1122 + hbv_main.ATldv_blast_assert.split_G4_177 == hbv_main.ATldv_blast_assert.split_O_40) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_T3_96[hbv_main.ATldv_blast_assert.split_U3_97 := hbv_main.ATldv_blast_assert.split_V3_98] != hbv_main.ATldv_blast_assert.split_W3_99)) && !(hbv_main.ATldv_blast_assert.split_R5_280[hbv_main.ATldv_blast_assert.split_P5_281] != hbv_main.ATldv_blast_assert.split_T5_282 && hbv_main.ATldv_blast_assert.split_L6_106)) && !((hbv_main.ATldv_blast_assert.split_L16_197 && hbv_main.ATldv_blast_assert.split_H18_31) && !hbv_main.ATldv_blast_assert.split_J16_443)) && !(hbv_main.ATldv_blast_assert.split_B13_12 != hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_E1_37] && hbv_main.ATldv_blast_assert.split_O1_44)) && !(hbv_main.ATldv_blast_assert.split_H7_128[hbv_main.ATldv_blast_assert.split_B6_382] != hbv_main.ATldv_blast_assert.split_N6_259 && hbv_main.ATldv_blast_assert.split_L6_106)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && hbv_main.ATldv_blast_assert.split_C3_172 <= 0)) && !((hbv_main.ATldv_blast_assert.split_F19_507 && hbv_main.ATldv_blast_assert.split_Z19_247) && hbv_main.ATldv_blast_assert.split_A20_248)) && !((hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_Q9_211 <= 0) && 0 < hbv_main.ATldv_blast_assert.split_O10_68)) && hbv_main.ATldv_blast_assert.split_N1_498 == 16 + hbv_main.ATldv_blast_assert.split_D7_142) && !(hbv_main.ATldv_blast_assert.split_A9_384[hbv_main.ATldv_blast_assert.split_B9_67 := hbv_main.ATldv_blast_assert.split_C9_385] != hbv_main.ATldv_blast_assert.split_D9_386 && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_Z8_511 == hbv_main.ATldv_blast_assert.split_C9_385) && 1120 + hbv_main.ATldv_blast_assert.split_W11_146 == hbv_main.ATldv_blast_assert.split_I9_241) && !((hbv_main.ATldv_blast_assert.split_W16_136 && hbv_main.ATldv_blast_assert.split_X16_135) && hbv_main.ATldv_blast_assert.split_E17_218 != hbv_main.ATldv_blast_assert.split_U16_186)) && !((hbv_main.ATldv_blast_assert.split_P19_34 && hbv_main.ATldv_blast_assert.split_D20_35) && hbv_main.ATldv_blast_assert.split_O19_417 != hbv_main.ATldv_blast_assert.split_X19_246)) && hbv_main.ATldv_blast_assert.split_H4_195 == hbv_main.ATldv_blast_assert.split_F4_490) && hbv_main.ATldv_blast_assert.split_S9_171 == hbv_main.ATldv_blast_assert.split_T9_477) && hbv_main.ATldv_blast_assert.split_E16_166 == hbv_main.ATldv_blast_assert.split_Z15_301) && hbv_main.ATldv_blast_assert.split_L5_76 + 168 == hbv_main.ATldv_blast_assert.split_U4_127) && !(hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_R5_280[hbv_main.ATldv_blast_assert.split_S5_327 := hbv_main.ATldv_blast_assert.split_T5_282] != hbv_main.ATldv_blast_assert.split_W5_381)) && !(hbv_main.ATldv_blast_assert.split_X8_344 != hbv_main.ATldv_blast_assert.split_U8_343[hbv_main.ATldv_blast_assert.split_V8_286 := hbv_main.ATldv_blast_assert.split_H11_116] && hbv_main.ATldv_blast_assert.split_O1_44)) && hbv_main.ATldv_blast_assert.split_H1_141 == 32 + hbv_main.ATldv_blast_assert.split_D7_142) && !(hbv_main.ATldv_blast_assert.split_A1_274 && hbv_main.ATldv_blast_assert.split_Q_439)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_V14_250] != hbv_main.ATldv_blast_assert.split_N11_59)) && !(hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_W5_381[hbv_main.ATldv_blast_assert.split_X5_357 := hbv_main.ATldv_blast_assert.split_Y5_413] != hbv_main.ATldv_blast_assert.split_H7_128)) && hbv_main.ATldv_blast_assert.split_H7_128 == hbv_main.ATldv_blast_assert.split_K7_129) && hbv_main.ATldv_blast_assert.split_H17_28 == hbv_main.ATldv_blast_assert.split_Z16_270) && !(hbv_main.ATldv_blast_assert.split_D18_150 && (!hbv_main.ATldv_blast_assert.split_S_5 || !hbv_main.ATldv_blast_assert.split_D18_150))) && !((!hbv_main.ATldv_blast_assert.split_A16_291 || !hbv_main.ATldv_blast_assert.split_C16_168) && hbv_main.ATldv_blast_assert.split_A16_291)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_K9_43[hbv_main.ATldv_blast_assert.split_J9_348] != hbv_main.ATldv_blast_assert.split_M9_349)) && !(hbv_main.ATldv_blast_assert.split_O4_196 < 5 && !hbv_main.ATldv_blast_assert.split_N4_209)) && !!hbv_main.ATldv_blast_assert.split_E20_228) && !((hbv_main.ATldv_blast_assert.split_G_313 || hbv_main.ATldv_blast_assert.split_B_383 == 0) && (hbv_main.ATldv_blast_assert.split_B_383 != 0 || !hbv_main.ATldv_blast_assert.split_G_313))) && 16 + hbv_main.ATldv_blast_assert.split_C3_172 == hbv_main.ATldv_blast_assert.split_D3_173) && hbv_main.ATldv_blast_assert.split_T7_255 == hbv_main.ATldv_blast_assert.split_D7_142) && hbv_main.ATldv_blast_assert.split_W_325 == hbv_main.ATldv_blast_assert.split_T_159) && !(hbv_main.ATldv_blast_assert.split_I6_306 <= 0 && hbv_main.ATldv_blast_assert.split_J6_305)) && !((hbv_main.ATldv_blast_assert.split_V6_154 != hbv_main.ATldv_blast_assert.split_W6_155 && hbv_main.ATldv_blast_assert.split_T6_89) && hbv_main.ATldv_blast_assert.split_U6_88)) && hbv_main.ATldv_blast_assert.split_X7_234 == hbv_main.ATldv_blast_assert.split_B8_235) && !((!hbv_main.ATldv_blast_assert.split_M6_492 && hbv_main.ATldv_blast_assert.split_Y6_102) && hbv_main.ATldv_blast_assert.split_L6_106)) && !((hbv_main.ATldv_blast_assert.split_W16_136 && hbv_main.ATldv_blast_assert.split_X16_135) && hbv_main.ATldv_blast_assert.split_G17_374 != hbv_main.ATldv_blast_assert.split_Y16_455)) && !(hbv_main.ATldv_blast_assert.split_V_38 <= 0 && hbv_main.ATldv_blast_assert.split_J1_27)) && !(((!hbv_main.ATldv_blast_assert.split_L7_238 || !hbv_main.ATldv_blast_assert.split_R6_152) && hbv_main.ATldv_blast_assert.split_L7_238) && (!hbv_main.ATldv_blast_assert.split_U6_88 || !hbv_main.ATldv_blast_assert.split_T6_89))) && hbv_main.ATldv_blast_assert.split_G15_7 == hbv_main.ATldv_blast_assert.split_Q15_151) && !((hbv_main.ATldv_blast_assert.split_L7_238 && hbv_main.ATldv_blast_assert.split_C8_239) && hbv_main.ATldv_blast_assert.split_V7_261 != hbv_main.ATldv_blast_assert.split_K7_129)) && !(hbv_main.ATldv_blast_assert.split_L6_106 && hbv_main.ATldv_blast_assert.split_Q5_326 <= 0)) && hbv_main.ATldv_blast_assert.split_P17_217 == hbv_main.ATldv_blast_assert.split_E17_218) && !((hbv_main.ATldv_blast_assert.split_S18_403 && hbv_main.ATldv_blast_assert.split_Z19_247) && !hbv_main.ATldv_blast_assert.split_F19_507)) && !(!hbv_main.ATldv_blast_assert.split_B17_182 && hbv_main.ATldv_blast_assert.split_C17_181)) && hbv_main.ATldv_blast_assert.split_K17_139 == hbv_main.ATldv_blast_assert.split_M14_473) && hbv_main.ATldv_blast_assert.split_I19_118 == hbv_main.ATldv_blast_assert.split_U19_190) && !(hbv_main.ATldv_blast_assert.split_H17_28[hbv_main.ATldv_blast_assert.split_O16_29 := 0] != hbv_main.ATldv_blast_assert.split_M17_30 && hbv_main.ATldv_blast_assert.split_H18_31)) && hbv_main.ATldv_blast_assert.split_I19_118 == hbv_main.ATldv_blast_assert.split_R18_368) && hbv_main.ATldv_blast_assert.split_K16_46 == hbv_main.ATldv_blast_assert.split_N_465) && !(((hbv_main.ATldv_blast_assert.split_J8_273 && hbv_main.ATldv_blast_assert.split_A1_274) && (!hbv_main.ATldv_blast_assert.split_L_450 || !hbv_main.ATldv_blast_assert.split_Q_439)) && (hbv_main.ATldv_blast_assert.split_L_450 || hbv_main.ATldv_blast_assert.split_Q_439))) && !((hbv_main.ATldv_blast_assert.split_B14_294 && hbv_main.ATldv_blast_assert.split_A14_295) && !hbv_main.ATldv_blast_assert.split_W13_345)) && hbv_main.ATldv_blast_assert.split_I3_311 == hbv_main.ATldv_blast_assert.split_F3_422) && !((hbv_main.ATldv_blast_assert.split_B14_294 && hbv_main.ATldv_blast_assert.split_A14_295) && hbv_main.ATldv_blast_assert.split_D14_292 != hbv_main.ATldv_blast_assert.split_C14_293)) && !(hbv_main.ATldv_blast_assert.split_D12_487 && 5 <= hbv_main.ATldv_blast_assert.split_E12_339)) && !(hbv_main.ATldv_blast_assert.split_O1_44 && hbv_main.ATldv_blast_assert.split_F11_115[hbv_main.ATldv_blast_assert.split_V10_512] != hbv_main.ATldv_blast_assert.split_W10_50)) && !((hbv_main.ATldv_blast_assert.split_B18_335 != hbv_main.ATldv_blast_assert.split_J18_69 && hbv_main.ATldv_blast_assert.split_O18_71) && hbv_main.ATldv_blast_assert.split_D18_150)) && !((hbv_main.ATldv_blast_assert.split_Z6_104 && hbv_main.ATldv_blast_assert.split_T6_89) && hbv_main.ATldv_blast_assert.split_Y6_102)) && !((!hbv_main.ATldv_blast_assert.split_T18_119 || !hbv_main.ATldv_blast_assert.split_Z19_247) && hbv_main.ATldv_blast_assert.split_Z19_247)) && !(hbv_main.ATldv_blast_assert.split_Z4_194[hbv_main.ATldv_blast_assert.split_A5_243 := hbv_main.ATldv_blast_assert.split_B5_491] != hbv_main.ATldv_blast_assert.split_E5_364 && hbv_main.ATldv_blast_assert.split_J5_224)) && !(hbv_main.ATldv_blast_assert.split_I4_52 && (!hbv_main.ATldv_blast_assert.split_A7_53 || !hbv_main.ATldv_blast_assert.split_I4_52));
      VAL   [hbv_main.ATldv_blast_assert.split_C10_277=274877939713, hbv_main.ATldv_blast_assert.split_F10_523=274877939732, hbv_main.ATldv_blast_assert.split_I_469=49, hbv_main.ATldv_blast_assert.split_J14_445=0, hbv_main.ATldv_blast_assert.split_N17_132=0, hbv_main.ATldv_blast_assert.split_O17_130=0, hbv_main.ATldv_blast_assert.split_P10_434=1, hbv_main.ATldv_blast_assert.split_Q10_394=9, hbv_main.ATldv_blast_assert.split_S11_63=1073742032, hbv_main.ATldv_blast_assert.split_Z8_511=274877939717, hbv_main.ATldv_blast_assert.split_Z9_519=49]
[L0]  CALL  call main.ATNodeBlock.i.us45(hbv_main.ATldv_blast_assert.split_H17_28, hbv_main.ATldv_blast_assert.split_N17_132, hbv_main.ATldv_blast_assert.split_O17_130, hbv_main.ATldv_blast_assert.split_J14_445, hbv_main.ATldv_blast_assert.split_Z8_511, hbv_main.ATldv_blast_assert.split_Z9_519, hbv_main.ATldv_blast_assert.split_C10_277, hbv_main.ATldv_blast_assert.split_F10_523, hbv_main.ATldv_blast_assert.split_P10_434, hbv_main.ATldv_blast_assert.split_Q10_394, hbv_main.ATldv_blast_assert.split_S11_63, hbv_main.ATldv_blast_assert.split_I_469, hbv_main.ATldv_blast_assert.split_A_525);
      VAL   [hhv_main.ATNodeBlock.i.us45_H_1=0, hhv_main.ATNodeBlock.i.us45_I_2=0, hhv_main.ATNodeBlock.i.us45_J_3=0, hhv_main.ATNodeBlock.i.us45_K_4=274877939717, hhv_main.ATNodeBlock.i.us45_L_5=49, hhv_main.ATNodeBlock.i.us45_M_6=274877939713, hhv_main.ATNodeBlock.i.us45_N_7=274877939732, hhv_main.ATNodeBlock.i.us45_O_8=1, hhv_main.ATNodeBlock.i.us45_P_9=9, hhv_main.ATNodeBlock.i.us45_Q_10=1073742032, hhv_main.ATNodeBlock.i.us45_R_11=49]
[L0]        assume (((((!!hbv_main.ATNodeBlock.i.us45_F_1 && !(hbv_main.ATNodeBlock.i.us45_E_2 && (!hbv_main.ATNodeBlock.i.us45_C_4 || !hbv_main.ATNodeBlock.i.us45_E_2))) && !((hbv_main.ATNodeBlock.i.us45_B_5 || hhv_main.ATNodeBlock.i.us45_J_3 == 1) && (!hbv_main.ATNodeBlock.i.us45_B_5 || hhv_main.ATNodeBlock.i.us45_J_3 != 1))) && !((!hbv_main.ATNodeBlock.i.us45_A_3 || !hbv_main.ATNodeBlock.i.us45_C_4) && hbv_main.ATNodeBlock.i.us45_C_4)) && !(hbv_main.ATNodeBlock.i.us45_F_1 && (!hbv_main.ATNodeBlock.i.us45_F_1 || !hbv_main.ATNodeBlock.i.us45_E_2))) && !((hbv_main.ATNodeBlock.i.us45_B_5 && hbv_main.ATNodeBlock.i.us45_C_4) && hbv_main.ATNodeBlock.i.us45_A_3)) && !((!hbv_main.ATNodeBlock.i.us45_D_6 && hbv_main.ATNodeBlock.i.us45_C_4) && hbv_main.ATNodeBlock.i.us45_E_2);
      VAL   [hbv_main.ATNodeBlock.i.us45_D_6=true, hhv_main.ATNodeBlock.i.us45_H_1=0, hhv_main.ATNodeBlock.i.us45_I_2=0, hhv_main.ATNodeBlock.i.us45_J_3=0, hhv_main.ATNodeBlock.i.us45_K_4=274877939717, hhv_main.ATNodeBlock.i.us45_L_5=49, hhv_main.ATNodeBlock.i.us45_M_6=274877939713, hhv_main.ATNodeBlock.i.us45_N_7=274877939732, hhv_main.ATNodeBlock.i.us45_O_8=1, hhv_main.ATNodeBlock.i.us45_P_9=9, hhv_main.ATNodeBlock.i.us45_Q_10=1073742032, hhv_main.ATNodeBlock.i.us45_R_11=49]
[L0]  CALL  call main.ATNodeBlock.i.lr.ph(hhv_main.ATNodeBlock.i.us45_G_0, hhv_main.ATNodeBlock.i.us45_H_1, hhv_main.ATNodeBlock.i.us45_I_2, hbv_main.ATNodeBlock.i.us45_D_6, hhv_main.ATNodeBlock.i.us45_J_3, hhv_main.ATNodeBlock.i.us45_K_4, hhv_main.ATNodeBlock.i.us45_L_5, hhv_main.ATNodeBlock.i.us45_M_6, hhv_main.ATNodeBlock.i.us45_N_7, hhv_main.ATNodeBlock.i.us45_O_8, hhv_main.ATNodeBlock.i.us45_P_9, hhv_main.ATNodeBlock.i.us45_Q_10, hhv_main.ATNodeBlock.i.us45_R_11, hhv_main.ATNodeBlock.i.us45_S_12);
      VAL   [hhv_main.ATNodeBlock.i.lr.ph_A1_4=0, hhv_main.ATNodeBlock.i.lr.ph_B1_5=274877939717, hhv_main.ATNodeBlock.i.lr.ph_C1_6=49, hhv_main.ATNodeBlock.i.lr.ph_D1_7=274877939713, hhv_main.ATNodeBlock.i.lr.ph_E1_8=274877939732, hhv_main.ATNodeBlock.i.lr.ph_F1_9=1, hhv_main.ATNodeBlock.i.lr.ph_G1_10=9, hhv_main.ATNodeBlock.i.lr.ph_H1_11=1073742032, hhv_main.ATNodeBlock.i.lr.ph_I1_12=49, hhv_main.ATNodeBlock.i.lr.ph_X_1=0, hhv_main.ATNodeBlock.i.lr.ph_Y_2=0, hhv_main.ATNodeBlock.i.lr.ph_Z_3=true]
[L0]        assume ((((((((((((((((((((((((((!((!hbv_main.ATNodeBlock.i.lr.ph_H_16 && hbv_main.ATNodeBlock.i.lr.ph_J_8) && hbv_main.ATNodeBlock.i.lr.ph_G_13) && !((0 < hhv_main.ATNodeBlock.i.lr.ph_F1_9 && hhv_main.ATNodeBlock.i.lr.ph_G1_10 <= 0) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && hbv_main.ATNodeBlock.i.lr.ph_V_15 == 0) && !((0 < hhv_main.ATNodeBlock.i.lr.ph_F1_9 && hhv_main.ATNodeBlock.i.lr.ph_C1_6 <= 0) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && hhv_main.ATNodeBlock.i.lr.ph_F1_9 + 8 == hhv_main.ATNodeBlock.i.lr.ph_G1_10) && !((hbv_main.ATNodeBlock.i.lr.ph_T_6 && hbv_main.ATNodeBlock.i.lr.ph_U_3) && hbv_main.ATNodeBlock.i.lr.ph_P_12 != hhv_main.ATNodeBlock.i.lr.ph_W_0)) && hhv_main.ATNodeBlock.i.lr.ph_C1_6 == hhv_main.ATNodeBlock.i.lr.ph_F1_9 + 48) && !!hbv_main.ATNodeBlock.i.lr.ph_S_10) && !((hbv_main.ATNodeBlock.i.lr.ph_J_8 && hbv_main.ATNodeBlock.i.lr.ph_K_9) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && !((hhv_main.ATNodeBlock.i.lr.ph_A1_4 != hbv_main.ATNodeBlock.i.lr.ph_V_15 && hbv_main.ATNodeBlock.i.lr.ph_T_6) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && hbv_main.ATNodeBlock.i.lr.ph_O_1 == 0) && hhv_main.ATNodeBlock.i.lr.ph_I1_12 == hbv_main.ATNodeBlock.i.lr.ph_L_4) && !((hbv_main.ATNodeBlock.i.lr.ph_H_16 || hbv_main.ATNodeBlock.i.lr.ph_F_20 == 0) && (!hbv_main.ATNodeBlock.i.lr.ph_H_16 || hbv_main.ATNodeBlock.i.lr.ph_F_20 != 0))) && !((!hbv_main.ATNodeBlock.i.lr.ph_J_8 || !hbv_main.ATNodeBlock.i.lr.ph_U_3) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && !!hbv_main.ATNodeBlock.i.lr.ph_T_6) && !((0 < hhv_main.ATNodeBlock.i.lr.ph_F1_9 && hbv_main.ATNodeBlock.i.lr.ph_U_3) && hbv_main.ATNodeBlock.i.lr.ph_L_4 <= 0)) && !(((hbv_main.ATNodeBlock.i.lr.ph_T_6 && hbv_main.ATNodeBlock.i.lr.ph_U_3) && (hhv_main.ATNodeBlock.i.lr.ph_Z_3 || hbv_main.ATNodeBlock.i.lr.ph_S_10)) && (!hbv_main.ATNodeBlock.i.lr.ph_S_10 || !hhv_main.ATNodeBlock.i.lr.ph_Z_3))) && !((hhv_main.ATNodeBlock.i.lr.ph_Y_2 != hbv_main.ATNodeBlock.i.lr.ph_R_5 && hbv_main.ATNodeBlock.i.lr.ph_T_6) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && hbv_main.ATNodeBlock.i.lr.ph_O_1 == hbv_main.ATNodeBlock.i.lr.ph_R_5) && hbv_main.ATNodeBlock.i.lr.ph_P_12 == hbv_main.ATNodeBlock.i.lr.ph_M_14) && hbv_main.ATNodeBlock.i.lr.ph_N_2 == 0) && hbv_main.ATNodeBlock.i.lr.ph_N_2 == hbv_main.ATNodeBlock.i.lr.ph_Q_7) && !((hbv_main.ATNodeBlock.i.lr.ph_K_9 || hbv_main.ATNodeBlock.i.lr.ph_I_11 == 0) && (!hbv_main.ATNodeBlock.i.lr.ph_K_9 || hbv_main.ATNodeBlock.i.lr.ph_I_11 != 0))) && !((hhv_main.ATNodeBlock.i.lr.ph_X_1 != hbv_main.ATNodeBlock.i.lr.ph_Q_7 && hbv_main.ATNodeBlock.i.lr.ph_T_6) && hbv_main.ATNodeBlock.i.lr.ph_U_3)) && !(hbv_main.ATNodeBlock.i.lr.ph_T_6 && (!hbv_main.ATNodeBlock.i.lr.ph_T_6 || !hbv_main.ATNodeBlock.i.lr.ph_U_3))) && hbv_main.ATNodeBlock.i.lr.ph_L_4 == hhv_main.ATNodeBlock.i.lr.ph_F1_9 + 48) && !((!hbv_main.ATNodeBlock.i.lr.ph_J_8 || !hbv_main.ATNodeBlock.i.lr.ph_G_13) && hbv_main.ATNodeBlock.i.lr.ph_J_8)) && hbv_main.ATNodeBlock.i.lr.ph_D_17[hbv_main.ATNodeBlock.i.lr.ph_E_18 := 16] == hbv_main.ATNodeBlock.i.lr.ph_C_19;
      VAL   [hhv_main.ATNodeBlock.i.lr.ph_A1_4=0, hhv_main.ATNodeBlock.i.lr.ph_B1_5=274877939717, hhv_main.ATNodeBlock.i.lr.ph_C1_6=49, hhv_main.ATNodeBlock.i.lr.ph_D1_7=274877939713, hhv_main.ATNodeBlock.i.lr.ph_E1_8=274877939732, hhv_main.ATNodeBlock.i.lr.ph_F1_9=1, hhv_main.ATNodeBlock.i.lr.ph_G1_10=9, hhv_main.ATNodeBlock.i.lr.ph_H1_11=1073742032, hhv_main.ATNodeBlock.i.lr.ph_I1_12=49, hhv_main.ATNodeBlock.i.lr.ph_X_1=0, hhv_main.ATNodeBlock.i.lr.ph_Y_2=0, hhv_main.ATNodeBlock.i.lr.ph_Z_3=true]
[L0]  CALL  call main.ATentry(hhv_main.ATNodeBlock.i.lr.ph_D1_7, hhv_main.ATNodeBlock.i.lr.ph_E1_8, hhv_main.ATNodeBlock.i.lr.ph_H1_11, hbv_main.ATNodeBlock.i.lr.ph_M_14, hbv_main.ATNodeBlock.i.lr.ph_D_17, hbv_main.ATNodeBlock.i.lr.ph_A_21, hbv_main.ATNodeBlock.i.lr.ph_B_22);
[L0]  RET   call main.ATentry(hhv_main.ATNodeBlock.i.lr.ph_D1_7, hhv_main.ATNodeBlock.i.lr.ph_E1_8, hhv_main.ATNodeBlock.i.lr.ph_H1_11, hbv_main.ATNodeBlock.i.lr.ph_M_14, hbv_main.ATNodeBlock.i.lr.ph_D_17, hbv_main.ATNodeBlock.i.lr.ph_A_21, hbv_main.ATNodeBlock.i.lr.ph_B_22);
      VAL   [hbv_main.ATNodeBlock.i.lr.ph_A_21=274877939720, hbv_main.ATNodeBlock.i.lr.ph_B_22=274877939725, hhv_main.ATNodeBlock.i.lr.ph_A1_4=0, hhv_main.ATNodeBlock.i.lr.ph_B1_5=274877939717, hhv_main.ATNodeBlock.i.lr.ph_C1_6=49, hhv_main.ATNodeBlock.i.lr.ph_D1_7=274877939713, hhv_main.ATNodeBlock.i.lr.ph_E1_8=274877939732, hhv_main.ATNodeBlock.i.lr.ph_F1_9=1, hhv_main.ATNodeBlock.i.lr.ph_G1_10=9, hhv_main.ATNodeBlock.i.lr.ph_H1_11=1073742032, hhv_main.ATNodeBlock.i.lr.ph_I1_12=49, hhv_main.ATNodeBlock.i.lr.ph_X_1=0, hhv_main.ATNodeBlock.i.lr.ph_Y_2=0, hhv_main.ATNodeBlock.i.lr.ph_Z_3=true]
[L0]  RET   call main.ATNodeBlock.i.lr.ph(hhv_main.ATNodeBlock.i.us45_G_0, hhv_main.ATNodeBlock.i.us45_H_1, hhv_main.ATNodeBlock.i.us45_I_2, hbv_main.ATNodeBlock.i.us45_D_6, hhv_main.ATNodeBlock.i.us45_J_3, hhv_main.ATNodeBlock.i.us45_K_4, hhv_main.ATNodeBlock.i.us45_L_5, hhv_main.ATNodeBlock.i.us45_M_6, hhv_main.ATNodeBlock.i.us45_N_7, hhv_main.ATNodeBlock.i.us45_O_8, hhv_main.ATNodeBlock.i.us45_P_9, hhv_main.ATNodeBlock.i.us45_Q_10, hhv_main.ATNodeBlock.i.us45_R_11, hhv_main.ATNodeBlock.i.us45_S_12);
      VAL   [hbv_main.ATNodeBlock.i.us45_D_6=true, hhv_main.ATNodeBlock.i.us45_H_1=0, hhv_main.ATNodeBlock.i.us45_I_2=0, hhv_main.ATNodeBlock.i.us45_J_3=0, hhv_main.ATNodeBlock.i.us45_K_4=274877939717, hhv_main.ATNodeBlock.i.us45_L_5=49, hhv_main.ATNodeBlock.i.us45_M_6=274877939713, hhv_main.ATNodeBlock.i.us45_N_7=274877939732, hhv_main.ATNodeBlock.i.us45_O_8=1, hhv_main.ATNodeBlock.i.us45_P_9=9, hhv_main.ATNodeBlock.i.us45_Q_10=1073742032, hhv_main.ATNodeBlock.i.us45_R_11=49]
[L0]  RET   call main.ATNodeBlock.i.us45(hbv_main.ATldv_blast_assert.split_H17_28, hbv_main.ATldv_blast_assert.split_N17_132, hbv_main.ATldv_blast_assert.split_O17_130, hbv_main.ATldv_blast_assert.split_J14_445, hbv_main.ATldv_blast_assert.split_Z8_511, hbv_main.ATldv_blast_assert.split_Z9_519, hbv_main.ATldv_blast_assert.split_C10_277, hbv_main.ATldv_blast_assert.split_F10_523, hbv_main.ATldv_blast_assert.split_P10_434, hbv_main.ATldv_blast_assert.split_Q10_394, hbv_main.ATldv_blast_assert.split_S11_63, hbv_main.ATldv_blast_assert.split_I_469, hbv_main.ATldv_blast_assert.split_A_525);
      VAL   [hbv_main.ATldv_blast_assert.split_C10_277=274877939713, hbv_main.ATldv_blast_assert.split_F10_523=274877939732, hbv_main.ATldv_blast_assert.split_I_469=49, hbv_main.ATldv_blast_assert.split_J14_445=0, hbv_main.ATldv_blast_assert.split_N17_132=0, hbv_main.ATldv_blast_assert.split_O17_130=0, hbv_main.ATldv_blast_assert.split_P10_434=1, hbv_main.ATldv_blast_assert.split_Q10_394=9, hbv_main.ATldv_blast_assert.split_S11_63=1073742032, hbv_main.ATldv_blast_assert.split_Z8_511=274877939717, hbv_main.ATldv_blast_assert.split_Z9_519=49]
[L0]  RET   call main.ATldv_blast_assert.split();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 8 procedures, 36 locations, 61 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.6s, OverallIterations: 3, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 3 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 1 mSDsluCounter, 150 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 68 mSDsCounter, 1 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 11 IncrementalHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 1 mSolverCounterUnsat, 82 mSDtfsCounter, 11 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 6 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=36occurred in iteration=0, InterpolantAutomatonStates: 6, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.0s AutomataMinimizationTime, 2 MinimizatonAttempts, 0 StatesRemovedByMinimization, 0 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 1.4s SatisfiabilityAnalysisTime, 0.6s InterpolantComputationTime, 43 NumberOfCodeBlocks, 43 NumberOfCodeBlocksAsserted, 3 NumberOfCheckSat, 22 ConstructedInterpolants, 0 QuantifiedInterpolants, 23 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 2 InterpolantComputations, 2 PerfectInterpolantSequences, 0/0 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
RESULT: Ultimate proved your program to be incorrect!
[2025-04-28 21:21:55,867 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
unsat
