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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:11,202 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:11,309 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5d202ae5-8763-462d-ba1d-00a77643b201/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:11,320 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:11,323 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:11,362 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:11,364 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:11,365 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:11,367 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:11,367 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:11,367 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:11,367 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:11,368 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:11,368 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:11,368 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:11,369 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:11,370 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:11,370 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:11,370 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:11,371 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:11,371 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:11,371 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:11,371 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:11,371 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:11,371 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:11,372 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:11,372 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:11,768 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:11,781 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:11,786 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:11,789 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:11,790 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:11,791 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5d202ae5-8763-462d-ba1d-00a77643b201/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-075.smt2
[2025-04-28 21:21:11,794 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:11,802 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:12,217 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5d202ae5-8763-462d-ba1d-00a77643b201/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-075.smt2
[2025-04-28 21:21:12,225 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:12,227 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:12,228 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:12,228 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:12,229 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:12,236 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,300 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12 Unit
[2025-04-28 21:21:12,300 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:12,301 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,302 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:12,302 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:12,323 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,324 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,359 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,360 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,366 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,368 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,376 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,378 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,379 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,416 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,417 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:12,417 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:12,417 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:12,422 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,430 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:12,448 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:12,463 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:12,469 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:12,485 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:12,486 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:12,486 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:12,486 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:12,486 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:12,486 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:12,486 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:12,490 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:12,491 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:12,491 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:12,491 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:12,491 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:12,491 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:12,491 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:12,491 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:12,640 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:12,642 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:12,943 INFO  L?                        ?]: Removed 8 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:12,944 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:12,959 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:12,959 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:12,960 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12 BoogieIcfgContainer
[2025-04-28 21:21:12,960 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:12,965 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:12,965 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:12,970 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:12,970 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:12" (1/3) ...
[2025-04-28 21:21:12,971 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6b457464 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,972 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (2/3) ...
[2025-04-28 21:21:12,972 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6b457464 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,972 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12" (3/3) ...
[2025-04-28 21:21:12,974 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:12,993 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:12,996 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 22 locations, 36 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:13,070 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:13,095 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;@2590422d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:13,098 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:13,102 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 22 states, 9 states have (on average 1.6666666666666667) internal successors, (15), 12 states have internal predecessors, (15), 7 states have call successors, (7), 4 states have call predecessors, (7), 4 states have return successors, (7), 6 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:13,112 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:13,112 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,113 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:13,114 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,120 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,121 INFO  L85        PathProgramCache]: Analyzing trace with hash -283319153, now seen corresponding path program 1 times
[2025-04-28 21:21:13,132 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,132 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1996211169]
[2025-04-28 21:21:13,133 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,134 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,196 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:13,273 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:13,273 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,273 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,078 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:14,079 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,079 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1996211169]
[2025-04-28 21:21:14,080 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1996211169] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,080 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,085 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:14,087 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1398994267]
[2025-04-28 21:21:14,088 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,096 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:14,096 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,130 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:14,132 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:14,135 INFO  L87              Difference]: Start difference. First operand  has 22 states, 9 states have (on average 1.6666666666666667) internal successors, (15), 12 states have internal predecessors, (15), 7 states have call successors, (7), 4 states have call predecessors, (7), 4 states have return successors, (7), 6 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:14,322 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,323 INFO  L93              Difference]: Finished difference Result 26 states and 35 transitions.
[2025-04-28 21:21:14,325 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:14,327 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:14,327 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,335 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:14,338 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:14,340 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:14,346 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 2 mSDsluCounter, 77 mSDsCounter, 0 mSdLazyCounter, 36 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 36 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 36 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,349 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 101 Invalid, 36 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 36 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:14,395 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:14,431 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 22.
[2025-04-28 21:21:14,432 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 9 states have (on average 1.5555555555555556) internal successors, (14), 12 states have internal predecessors, (14), 7 states have call successors, (7), 4 states have call predecessors, (7), 5 states have return successors, (10), 6 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:14,446 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 31 transitions.
[2025-04-28 21:21:14,448 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 31 transitions. Word has length 16
[2025-04-28 21:21:14,449 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,449 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 31 transitions.
[2025-04-28 21:21:14,449 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:14,449 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 31 transitions.
[2025-04-28 21:21:14,458 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:14,458 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,458 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,458 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:14,459 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,459 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,460 INFO  L85        PathProgramCache]: Analyzing trace with hash 2074842907, now seen corresponding path program 1 times
[2025-04-28 21:21:14,460 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,460 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1399423604]
[2025-04-28 21:21:14,460 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,460 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,507 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:14,523 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:14,523 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,523 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,948 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:14,948 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1399423604]
[2025-04-28 21:21:14,949 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1399423604] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,949 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,949 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:14,949 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2105016391]
[2025-04-28 21:21:14,949 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,950 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:14,951 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,955 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:14,956 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:14,956 INFO  L87              Difference]: Start difference. First operand 22 states and 31 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:15,132 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:15,132 INFO  L93              Difference]: Finished difference Result 28 states and 39 transitions.
[2025-04-28 21:21:15,134 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:15,135 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:15,135 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:15,136 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:15,137 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:15,137 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:15,138 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 2 mSDsluCounter, 92 mSDsCounter, 0 mSdLazyCounter, 36 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 120 SdHoareTripleChecker+Invalid, 36 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 36 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:15,140 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 120 Invalid, 36 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 36 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:15,141 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:15,149 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 22.
[2025-04-28 21:21:15,149 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 9 states have (on average 1.5555555555555556) internal successors, (14), 12 states have internal predecessors, (14), 7 states have call successors, (7), 4 states have call predecessors, (7), 5 states have return successors, (10), 6 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:15,150 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 31 transitions.
[2025-04-28 21:21:15,150 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 31 transitions. Word has length 16
[2025-04-28 21:21:15,150 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:15,151 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 31 transitions.
[2025-04-28 21:21:15,151 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:15,151 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 31 transitions.
[2025-04-28 21:21:15,152 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:15,152 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,152 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,152 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:15,152 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,155 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,156 INFO  L85        PathProgramCache]: Analyzing trace with hash 1288788887, now seen corresponding path program 1 times
[2025-04-28 21:21:15,156 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,156 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [493617089]
[2025-04-28 21:21:15,156 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,156 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,171 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:15,185 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:15,185 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,185 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:15,185 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-04-28 21:21:15,197 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:15,212 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:15,213 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,213 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:15,255 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-04-28 21:21:15,256 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-04-28 21:21:15,257 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:15,261 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:15,265 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1]
[2025-04-28 21:21:15,293 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:15,296 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:15 BoogieIcfgContainer
[2025-04-28 21:21:15,296 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:15,297 INFO  L158              Benchmark]: Toolchain (without parser) took 3070.36ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 157.0MB in the beginning and 67.5MB in the end (delta: 89.6MB). Peak memory consumption was 36.3MB. Max. memory is 33.6GB.
[2025-04-28 21:21:15,298 INFO  L158              Benchmark]: SmtParser took 0.42ms. Allocated memory is still 234.9MB. Free memory was 172.7MB in the beginning and 172.1MB in the end (delta: 587.3kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:15,298 INFO  L158              Benchmark]: ChcToBoogie took 72.53ms. Allocated memory is still 234.9MB. Free memory was 157.0MB in the beginning and 155.3MB in the end (delta: 1.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:15,298 INFO  L158              Benchmark]: Boogie Preprocessor took 114.55ms. Allocated memory is still 234.9MB. Free memory was 155.3MB in the beginning and 152.9MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:15,299 INFO  L158              Benchmark]: RCFGBuilder took 543.27ms. Allocated memory is still 234.9MB. Free memory was 152.9MB in the beginning and 130.6MB in the end (delta: 22.3MB). Peak memory consumption was 33.6MB. Max. memory is 33.6GB.
[2025-04-28 21:21:15,299 INFO  L158              Benchmark]: TraceAbstraction took 2331.80ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 130.0MB in the beginning and 67.5MB in the end (delta: 62.5MB). Peak memory consumption was 2.7MB. Max. memory is 33.6GB.
[2025-04-28 21:21:15,304 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.42ms. Allocated memory is still 234.9MB. Free memory was 172.7MB in the beginning and 172.1MB in the end (delta: 587.3kB). There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 72.53ms. Allocated memory is still 234.9MB. Free memory was 157.0MB in the beginning and 155.3MB in the end (delta: 1.8MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 114.55ms. Allocated memory is still 234.9MB. Free memory was 155.3MB in the beginning and 152.9MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 543.27ms. Allocated memory is still 234.9MB. Free memory was 152.9MB in the beginning and 130.6MB in the end (delta: 22.3MB). Peak memory consumption was 33.6MB. Max. memory is 33.6GB.
 * TraceAbstraction took 2331.80ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 130.0MB in the beginning and 67.5MB in the end (delta: 62.5MB). Peak memory consumption was 2.7MB. 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 realizable();
[L0]        assume (((((((((((((((((((((((((((!hbv_realizable_v_32_11 && !!hbv_realizable_v_28_29) && !(((!hbv_realizable_B_18 || !hbv_realizable_Y_19) || !hbv_realizable_X_20) && ((hbv_realizable_X_20 && hbv_realizable_Y_19) || hbv_realizable_B_18))) && !!hbv_realizable_v_29_31) && !hbv_realizable_v_37_32) && !(((hbv_realizable_P_26 && hbv_realizable_Q_27) || hbv_realizable_F_28) && ((!hbv_realizable_P_26 || !hbv_realizable_F_28) || !hbv_realizable_Q_27))) && !!hbv_realizable_v_34_9) && !!hbv_realizable_v_30_36) && !((hbv_realizable_E_40 || (hbv_realizable_R_38 && hbv_realizable_S_39)) && ((!hbv_realizable_S_39 || !hbv_realizable_R_38) || !hbv_realizable_E_40))) && !hbv_realizable_v_41_35) && !hbv_realizable_v_43_21) && !(((!hbv_realizable_W_23 || hbv_realizable_C_24) || hbv_realizable_V_25) && ((hbv_realizable_W_23 && !hbv_realizable_V_25) || !hbv_realizable_C_24))) && !(((hbv_realizable_D_15 || hbv_realizable_T_16) || !hbv_realizable_U_17) && (!hbv_realizable_D_15 || (!hbv_realizable_T_16 && hbv_realizable_U_17)))) && !hbv_realizable_v_36_2) && !((!hbv_realizable_G_45 || (hbv_realizable_O_43 && !hbv_realizable_N_44)) && ((!hbv_realizable_O_43 || hbv_realizable_N_44) || hbv_realizable_G_45))) && hbv_realizable_v_27_42 == 0) && !!hbv_realizable_v_42_30) && !(((!hbv_realizable_Z_5 || !hbv_realizable_A_6) || !hbv_realizable_A1_7) && (hbv_realizable_A_6 || (hbv_realizable_A1_7 && hbv_realizable_Z_5)))) && !hbv_realizable_v_33_33) && !hbv_realizable_v_46_10) && !!hbv_realizable_v_40_34) && !hbv_realizable_v_39_8) && !hbv_realizable_v_47_41) && !!hbv_realizable_v_31_3) && !hbv_realizable_v_45_4) && !(((!hbv_realizable_L_12 || !hbv_realizable_H_13) || !hbv_realizable_M_14) && ((hbv_realizable_L_12 && hbv_realizable_M_14) || hbv_realizable_H_13))) && !hbv_realizable_v_44_22) && !hbv_realizable_v_38_1) && !hbv_realizable_v_35_37;
      VAL   [hbv_realizable_A1_7=false, hbv_realizable_A_6=false, hbv_realizable_B_18=false, hbv_realizable_C_24=true, hbv_realizable_D_15=true, hbv_realizable_E_40=false, hbv_realizable_F_28=false, hbv_realizable_G_45=true, hbv_realizable_H_13=false, hbv_realizable_M_14=false, hbv_realizable_O_43=false, hbv_realizable_Q_27=false, hbv_realizable_S_39=false, hbv_realizable_U_17=false, hbv_realizable_W_23=false, hbv_realizable_Y_19=false, hbv_realizable_v_27_42=0, hbv_realizable_v_28_29=true, hbv_realizable_v_29_31=true, hbv_realizable_v_30_36=true, hbv_realizable_v_31_3=true, hbv_realizable_v_32_11=false, hbv_realizable_v_33_33=false, hbv_realizable_v_34_9=true, hbv_realizable_v_35_37=false, hbv_realizable_v_36_2=false, hbv_realizable_v_37_32=false, hbv_realizable_v_38_1=false, hbv_realizable_v_39_8=false, hbv_realizable_v_40_34=true, hbv_realizable_v_41_35=false, hbv_realizable_v_42_30=true, hbv_realizable_v_43_21=false, hbv_realizable_v_44_22=false, hbv_realizable_v_45_4=false, hbv_realizable_v_46_10=false, hbv_realizable_v_47_41=false]
[L0]  CALL  call funcStart__syn(hbv_realizable_I_46, hbv_realizable_v_27_42, hbv_realizable_v_28_29, hbv_realizable_v_29_31, hbv_realizable_v_30_36, hbv_realizable_v_31_3, hbv_realizable_v_32_11, hbv_realizable_v_33_33, hbv_realizable_v_34_9, hbv_realizable_v_35_37, hbv_realizable_v_36_2, hbv_realizable_v_37_32, hbv_realizable_v_38_1, hbv_realizable_v_39_8, hbv_realizable_v_40_34, hbv_realizable_v_41_35, hbv_realizable_v_42_30, hbv_realizable_v_43_21, hbv_realizable_v_44_22, hbv_realizable_v_45_4, hbv_realizable_v_46_10, hbv_realizable_v_47_41, hbv_realizable_J_47, hbv_realizable_K_48, hbv_realizable_H_13, hbv_realizable_M_14, hbv_realizable_G_45, hbv_realizable_O_43, hbv_realizable_F_28, hbv_realizable_Q_27, hbv_realizable_E_40, hbv_realizable_S_39, hbv_realizable_D_15, hbv_realizable_U_17, hbv_realizable_C_24, hbv_realizable_W_23, hbv_realizable_B_18, hbv_realizable_Y_19, hbv_realizable_A_6, hbv_realizable_A1_7);
      VAL   [hhv_funcStart__syn_B1_13=false, hhv_funcStart__syn_C1_14=true, hhv_funcStart__syn_C_39=false, hhv_funcStart__syn_D1_15=false, hhv_funcStart__syn_D_38=false, hhv_funcStart__syn_E_35=false, hhv_funcStart__syn_F1_16=true, hhv_funcStart__syn_F_34=true, hhv_funcStart__syn_G1_4=true, hhv_funcStart__syn_G_31=false, hhv_funcStart__syn_H_30=false, hhv_funcStart__syn_I1_17=false, hhv_funcStart__syn_I_27=false, hhv_funcStart__syn_J1_18=false, hhv_funcStart__syn_J_26=true, hhv_funcStart__syn_K1_19=false, hhv_funcStart__syn_L_1=0, hhv_funcStart__syn_M1_20=false, hhv_funcStart__syn_N1_5=true, hhv_funcStart__syn_N_23=2, hhv_funcStart__syn_O_6=false, hhv_funcStart__syn_P1_21=false, hhv_funcStart__syn_P_7=false, hhv_funcStart__syn_R_8=true, hhv_funcStart__syn_S_2=true, hhv_funcStart__syn_U_9=false, hhv_funcStart__syn_V_10=false, hhv_funcStart__syn_W_11=false, hhv_funcStart__syn_Y_12=false, hhv_funcStart__syn_Z_3=true, hhv_funcStart__syn_v_42_24=false, hhv_funcStart__syn_v_43_25=false, hhv_funcStart__syn_v_44_28=false, hhv_funcStart__syn_v_45_29=false, hhv_funcStart__syn_v_46_32=true, hhv_funcStart__syn_v_47_33=false, hhv_funcStart__syn_v_48_36=false, hhv_funcStart__syn_v_49_37=false]
[L0]        assume ((((((((((((((((!((((hhv_funcStart__syn_W_11 || hhv_funcStart__syn_Z_3) && (hbv_funcStart__syn_Y_4 || !hhv_funcStart__syn_Z_3)) || hhv_funcStart__syn_v_45_29) && (((!hhv_funcStart__syn_W_11 && !hhv_funcStart__syn_Z_3) || !hhv_funcStart__syn_v_45_29) || (hhv_funcStart__syn_Z_3 && !hbv_funcStart__syn_Y_4))) && !((!hhv_funcStart__syn_B1_13 || !hhv_funcStart__syn_G_31) && (hhv_funcStart__syn_B1_13 || hhv_funcStart__syn_G_31))) && !((((!hhv_funcStart__syn_G1_4 && !hhv_funcStart__syn_C1_14) || !hhv_funcStart__syn_v_46_32) || (!hbv_funcStart__syn_Q_3 && hhv_funcStart__syn_G1_4)) && (((hhv_funcStart__syn_C1_14 || hhv_funcStart__syn_G1_4) && (hbv_funcStart__syn_Q_3 || !hhv_funcStart__syn_G1_4)) || hhv_funcStart__syn_v_46_32))) && !((!hhv_funcStart__syn_E_35 || !hhv_funcStart__syn_I1_17) && (hhv_funcStart__syn_I1_17 || hhv_funcStart__syn_E_35))) && !((!hhv_funcStart__syn_R_8 || !hhv_funcStart__syn_J_26) && (hhv_funcStart__syn_R_8 || hhv_funcStart__syn_J_26))) && !((hhv_funcStart__syn_v_49_37 || ((hbv_funcStart__syn_X_10 || !hhv_funcStart__syn_N1_5) && (hhv_funcStart__syn_N1_5 || hhv_funcStart__syn_K1_19))) && (((hhv_funcStart__syn_N1_5 && !hbv_funcStart__syn_X_10) || (!hhv_funcStart__syn_K1_19 && !hhv_funcStart__syn_N1_5)) || !hhv_funcStart__syn_v_49_37))) && !((((hhv_funcStart__syn_G1_4 && !hbv_funcStart__syn_E1_7) || (!hhv_funcStart__syn_D1_15 && !hhv_funcStart__syn_G1_4)) || !hhv_funcStart__syn_v_47_33) && (((hbv_funcStart__syn_E1_7 || !hhv_funcStart__syn_G1_4) && (hhv_funcStart__syn_G1_4 || hhv_funcStart__syn_D1_15)) || hhv_funcStart__syn_v_47_33))) && hbv_funcStart__syn_A_6 == hhv_funcStart__syn_L_1 + 1) && !(((!hhv_funcStart__syn_v_42_24 || (!hbv_funcStart__syn_T_2 && hhv_funcStart__syn_S_2)) || (!hhv_funcStart__syn_O_6 && !hhv_funcStart__syn_S_2)) && (((hhv_funcStart__syn_O_6 || hhv_funcStart__syn_S_2) && (hbv_funcStart__syn_T_2 || !hhv_funcStart__syn_S_2)) || hhv_funcStart__syn_v_42_24))) && !(((!hhv_funcStart__syn_v_44_28 || (hhv_funcStart__syn_Z_3 && !hbv_funcStart__syn_A1_1)) || (!hhv_funcStart__syn_V_10 && !hhv_funcStart__syn_Z_3)) && (((hhv_funcStart__syn_Z_3 || hhv_funcStart__syn_V_10) && (hbv_funcStart__syn_A1_1 || !hhv_funcStart__syn_Z_3)) || hhv_funcStart__syn_v_44_28))) && !((hhv_funcStart__syn_U_9 || hhv_funcStart__syn_I_27) && (!hhv_funcStart__syn_U_9 || !hhv_funcStart__syn_I_27))) && !((!hhv_funcStart__syn_H_30 || !hhv_funcStart__syn_Y_12) && (hhv_funcStart__syn_Y_12 || hhv_funcStart__syn_H_30))) && !((hhv_funcStart__syn_v_43_25 || ((hhv_funcStart__syn_P_7 || hhv_funcStart__syn_S_2) && (hbv_funcStart__syn_L1_8 || !hhv_funcStart__syn_S_2))) && (((!hbv_funcStart__syn_L1_8 && hhv_funcStart__syn_S_2) || !hhv_funcStart__syn_v_43_25) || (!hhv_funcStart__syn_P_7 && !hhv_funcStart__syn_S_2)))) && !((!hhv_funcStart__syn_M1_20 || !hhv_funcStart__syn_D_38) && (hhv_funcStart__syn_M1_20 || hhv_funcStart__syn_D_38))) && !((hhv_funcStart__syn_F1_16 || hhv_funcStart__syn_F_34) && (!hhv_funcStart__syn_F1_16 || !hhv_funcStart__syn_F_34))) && hbv_funcStart__syn_B_5 == hhv_funcStart__syn_K_0[hhv_funcStart__syn_L_1 := 0]) && !((((!hhv_funcStart__syn_J1_18 && !hhv_funcStart__syn_N1_5) || !hhv_funcStart__syn_v_48_36) || (!hbv_funcStart__syn_H1_9 && hhv_funcStart__syn_N1_5)) && (((hhv_funcStart__syn_J1_18 || hhv_funcStart__syn_N1_5) && (hbv_funcStart__syn_H1_9 || !hhv_funcStart__syn_N1_5)) || hhv_funcStart__syn_v_48_36))) && !((hhv_funcStart__syn_P1_21 || hhv_funcStart__syn_C_39) && (!hhv_funcStart__syn_C_39 || !hhv_funcStart__syn_P1_21));
      VAL   [hbv_funcStart__syn_A1_1=false, hbv_funcStart__syn_A_6=1, hbv_funcStart__syn_E1_7=false, hbv_funcStart__syn_H1_9=false, hbv_funcStart__syn_L1_8=false, hbv_funcStart__syn_Q_3=true, hbv_funcStart__syn_T_2=false, hbv_funcStart__syn_X_10=false, hbv_funcStart__syn_Y_4=false, hhv_funcStart__syn_B1_13=false, hhv_funcStart__syn_C1_14=true, hhv_funcStart__syn_C_39=false, hhv_funcStart__syn_D1_15=false, hhv_funcStart__syn_D_38=false, hhv_funcStart__syn_E_35=false, hhv_funcStart__syn_F1_16=true, hhv_funcStart__syn_F_34=true, hhv_funcStart__syn_G1_4=true, hhv_funcStart__syn_G_31=false, hhv_funcStart__syn_H_30=false, hhv_funcStart__syn_I1_17=false, hhv_funcStart__syn_I_27=false, hhv_funcStart__syn_J1_18=false, hhv_funcStart__syn_J_26=true, hhv_funcStart__syn_K1_19=false, hhv_funcStart__syn_L_1=0, hhv_funcStart__syn_M1_20=false, hhv_funcStart__syn_N1_5=true, hhv_funcStart__syn_N_23=2, hhv_funcStart__syn_O_6=false, hhv_funcStart__syn_P1_21=false, hhv_funcStart__syn_P_7=false, hhv_funcStart__syn_R_8=true, hhv_funcStart__syn_S_2=true, hhv_funcStart__syn_U_9=false, hhv_funcStart__syn_V_10=false, hhv_funcStart__syn_W_11=false, hhv_funcStart__syn_Y_12=false, hhv_funcStart__syn_Z_3=true, hhv_funcStart__syn_v_42_24=false, hhv_funcStart__syn_v_43_25=false, hhv_funcStart__syn_v_44_28=false, hhv_funcStart__syn_v_45_29=false, hhv_funcStart__syn_v_46_32=true, hhv_funcStart__syn_v_47_33=false, hhv_funcStart__syn_v_48_36=false, hhv_funcStart__syn_v_49_37=false]
[L0]  CALL  call funcE__syn(hbv_funcStart__syn_B_5, hbv_funcStart__syn_A_6, hhv_funcStart__syn_S_2, hhv_funcStart__syn_Z_3, hhv_funcStart__syn_G1_4, hhv_funcStart__syn_N1_5, hhv_funcStart__syn_O_6, hhv_funcStart__syn_P_7, hhv_funcStart__syn_R_8, hhv_funcStart__syn_U_9, hhv_funcStart__syn_V_10, hhv_funcStart__syn_W_11, hhv_funcStart__syn_Y_12, hhv_funcStart__syn_B1_13, hhv_funcStart__syn_C1_14, hhv_funcStart__syn_D1_15, hhv_funcStart__syn_F1_16, hhv_funcStart__syn_I1_17, hhv_funcStart__syn_J1_18, hhv_funcStart__syn_K1_19, hhv_funcStart__syn_M1_20, hhv_funcStart__syn_P1_21, hhv_funcStart__syn_M_22, hhv_funcStart__syn_N_23, hbv_funcStart__syn_T_2, hbv_funcStart__syn_L1_8, hbv_funcStart__syn_A1_1, hbv_funcStart__syn_Y_4, hbv_funcStart__syn_Q_3, hbv_funcStart__syn_E1_7, hbv_funcStart__syn_H1_9, hbv_funcStart__syn_X_10);
      VAL   [hhv_funcE__syn_B_1=1, hhv_funcE__syn_C_2=true, hhv_funcE__syn_D_3=true, hhv_funcE__syn_E_4=true, hhv_funcE__syn_F_5=true, hhv_funcE__syn_G_8=true, hhv_funcE__syn_H_9=false, hhv_funcE__syn_I_12=false, hhv_funcE__syn_J_13=false, hhv_funcE__syn_K_16=true, hhv_funcE__syn_L_17=false, hhv_funcE__syn_M_20=false, hhv_funcE__syn_N_21=false, hhv_funcE__syn_P_23=2, hhv_funcE__syn_Q_6=false, hhv_funcE__syn_R_7=false, hhv_funcE__syn_S_10=false, hhv_funcE__syn_T_11=false, hhv_funcE__syn_U_14=true, hhv_funcE__syn_V_15=false, hhv_funcE__syn_W_18=false, hhv_funcE__syn_X_19=false, hhv_funcE__syn_v_24_24=false, hhv_funcE__syn_v_25_25=false, hhv_funcE__syn_v_26_26=false, hhv_funcE__syn_v_27_27=false, hhv_funcE__syn_v_28_28=true, hhv_funcE__syn_v_29_29=false, hhv_funcE__syn_v_30_30=false, hhv_funcE__syn_v_31_31=false]
[L0]        assume ((((((((hhv_funcE__syn_A_0[hhv_funcE__syn_B_1 := 2] == hhv_funcE__syn_O_22 && hhv_funcE__syn_B_1 + 1 == hhv_funcE__syn_P_23) && !((hhv_funcE__syn_X_19 || hhv_funcE__syn_v_31_31) && (!hhv_funcE__syn_X_19 || !hhv_funcE__syn_v_31_31))) && !((hhv_funcE__syn_U_14 || hhv_funcE__syn_v_28_28) && (!hhv_funcE__syn_v_28_28 || !hhv_funcE__syn_U_14))) && !((!hhv_funcE__syn_v_25_25 || !hhv_funcE__syn_R_7) && (hhv_funcE__syn_R_7 || hhv_funcE__syn_v_25_25))) && !((hhv_funcE__syn_Q_6 || hhv_funcE__syn_v_24_24) && (!hhv_funcE__syn_v_24_24 || !hhv_funcE__syn_Q_6))) && !((hhv_funcE__syn_V_15 || hhv_funcE__syn_v_29_29) && (!hhv_funcE__syn_v_29_29 || !hhv_funcE__syn_V_15))) && !((hhv_funcE__syn_S_10 || hhv_funcE__syn_v_26_26) && (!hhv_funcE__syn_v_26_26 || !hhv_funcE__syn_S_10))) && !((hhv_funcE__syn_W_18 || hhv_funcE__syn_v_30_30) && (!hhv_funcE__syn_v_30_30 || !hhv_funcE__syn_W_18))) && !((hhv_funcE__syn_T_11 || hhv_funcE__syn_v_27_27) && (!hhv_funcE__syn_T_11 || !hhv_funcE__syn_v_27_27));
      VAL   [hhv_funcE__syn_B_1=1, hhv_funcE__syn_C_2=true, hhv_funcE__syn_D_3=true, hhv_funcE__syn_E_4=true, hhv_funcE__syn_F_5=true, hhv_funcE__syn_G_8=true, hhv_funcE__syn_H_9=false, hhv_funcE__syn_I_12=false, hhv_funcE__syn_J_13=false, hhv_funcE__syn_K_16=true, hhv_funcE__syn_L_17=false, hhv_funcE__syn_M_20=false, hhv_funcE__syn_N_21=false, hhv_funcE__syn_P_23=2, hhv_funcE__syn_Q_6=false, hhv_funcE__syn_R_7=false, hhv_funcE__syn_S_10=false, hhv_funcE__syn_T_11=false, hhv_funcE__syn_U_14=true, hhv_funcE__syn_V_15=false, hhv_funcE__syn_W_18=false, hhv_funcE__syn_X_19=false, hhv_funcE__syn_v_24_24=false, hhv_funcE__syn_v_25_25=false, hhv_funcE__syn_v_26_26=false, hhv_funcE__syn_v_27_27=false, hhv_funcE__syn_v_28_28=true, hhv_funcE__syn_v_29_29=false, hhv_funcE__syn_v_30_30=false, hhv_funcE__syn_v_31_31=false]
[L0]  RET   call funcE__syn(hbv_funcStart__syn_B_5, hbv_funcStart__syn_A_6, hhv_funcStart__syn_S_2, hhv_funcStart__syn_Z_3, hhv_funcStart__syn_G1_4, hhv_funcStart__syn_N1_5, hhv_funcStart__syn_O_6, hhv_funcStart__syn_P_7, hhv_funcStart__syn_R_8, hhv_funcStart__syn_U_9, hhv_funcStart__syn_V_10, hhv_funcStart__syn_W_11, hhv_funcStart__syn_Y_12, hhv_funcStart__syn_B1_13, hhv_funcStart__syn_C1_14, hhv_funcStart__syn_D1_15, hhv_funcStart__syn_F1_16, hhv_funcStart__syn_I1_17, hhv_funcStart__syn_J1_18, hhv_funcStart__syn_K1_19, hhv_funcStart__syn_M1_20, hhv_funcStart__syn_P1_21, hhv_funcStart__syn_M_22, hhv_funcStart__syn_N_23, hbv_funcStart__syn_T_2, hbv_funcStart__syn_L1_8, hbv_funcStart__syn_A1_1, hbv_funcStart__syn_Y_4, hbv_funcStart__syn_Q_3, hbv_funcStart__syn_E1_7, hbv_funcStart__syn_H1_9, hbv_funcStart__syn_X_10);
      VAL   [hbv_funcStart__syn_A1_1=false, hbv_funcStart__syn_A_6=1, hbv_funcStart__syn_E1_7=false, hbv_funcStart__syn_H1_9=false, hbv_funcStart__syn_L1_8=false, hbv_funcStart__syn_Q_3=true, hbv_funcStart__syn_T_2=false, hbv_funcStart__syn_X_10=false, hbv_funcStart__syn_Y_4=false, hhv_funcStart__syn_B1_13=false, hhv_funcStart__syn_C1_14=true, hhv_funcStart__syn_C_39=false, hhv_funcStart__syn_D1_15=false, hhv_funcStart__syn_D_38=false, hhv_funcStart__syn_E_35=false, hhv_funcStart__syn_F1_16=true, hhv_funcStart__syn_F_34=true, hhv_funcStart__syn_G1_4=true, hhv_funcStart__syn_G_31=false, hhv_funcStart__syn_H_30=false, hhv_funcStart__syn_I1_17=false, hhv_funcStart__syn_I_27=false, hhv_funcStart__syn_J1_18=false, hhv_funcStart__syn_J_26=true, hhv_funcStart__syn_K1_19=false, hhv_funcStart__syn_L_1=0, hhv_funcStart__syn_M1_20=false, hhv_funcStart__syn_N1_5=true, hhv_funcStart__syn_N_23=2, hhv_funcStart__syn_O_6=false, hhv_funcStart__syn_P1_21=false, hhv_funcStart__syn_P_7=false, hhv_funcStart__syn_R_8=true, hhv_funcStart__syn_S_2=true, hhv_funcStart__syn_U_9=false, hhv_funcStart__syn_V_10=false, hhv_funcStart__syn_W_11=false, hhv_funcStart__syn_Y_12=false, hhv_funcStart__syn_Z_3=true, hhv_funcStart__syn_v_42_24=false, hhv_funcStart__syn_v_43_25=false, hhv_funcStart__syn_v_44_28=false, hhv_funcStart__syn_v_45_29=false, hhv_funcStart__syn_v_46_32=true, hhv_funcStart__syn_v_47_33=false, hhv_funcStart__syn_v_48_36=false, hhv_funcStart__syn_v_49_37=false]
[L0]  RET   call funcStart__syn(hbv_realizable_I_46, hbv_realizable_v_27_42, hbv_realizable_v_28_29, hbv_realizable_v_29_31, hbv_realizable_v_30_36, hbv_realizable_v_31_3, hbv_realizable_v_32_11, hbv_realizable_v_33_33, hbv_realizable_v_34_9, hbv_realizable_v_35_37, hbv_realizable_v_36_2, hbv_realizable_v_37_32, hbv_realizable_v_38_1, hbv_realizable_v_39_8, hbv_realizable_v_40_34, hbv_realizable_v_41_35, hbv_realizable_v_42_30, hbv_realizable_v_43_21, hbv_realizable_v_44_22, hbv_realizable_v_45_4, hbv_realizable_v_46_10, hbv_realizable_v_47_41, hbv_realizable_J_47, hbv_realizable_K_48, hbv_realizable_H_13, hbv_realizable_M_14, hbv_realizable_G_45, hbv_realizable_O_43, hbv_realizable_F_28, hbv_realizable_Q_27, hbv_realizable_E_40, hbv_realizable_S_39, hbv_realizable_D_15, hbv_realizable_U_17, hbv_realizable_C_24, hbv_realizable_W_23, hbv_realizable_B_18, hbv_realizable_Y_19, hbv_realizable_A_6, hbv_realizable_A1_7);
      VAL   [hbv_realizable_A1_7=false, hbv_realizable_A_6=false, hbv_realizable_B_18=false, hbv_realizable_C_24=true, hbv_realizable_D_15=true, hbv_realizable_E_40=false, hbv_realizable_F_28=false, hbv_realizable_G_45=true, hbv_realizable_H_13=false, hbv_realizable_K_48=2, hbv_realizable_M_14=false, hbv_realizable_O_43=false, hbv_realizable_Q_27=false, hbv_realizable_S_39=false, hbv_realizable_U_17=false, hbv_realizable_W_23=false, hbv_realizable_Y_19=false, hbv_realizable_v_27_42=0, hbv_realizable_v_28_29=true, hbv_realizable_v_29_31=true, hbv_realizable_v_30_36=true, hbv_realizable_v_31_3=true, hbv_realizable_v_32_11=false, hbv_realizable_v_33_33=false, hbv_realizable_v_34_9=true, hbv_realizable_v_35_37=false, hbv_realizable_v_36_2=false, hbv_realizable_v_37_32=false, hbv_realizable_v_38_1=false, hbv_realizable_v_39_8=false, hbv_realizable_v_40_34=true, hbv_realizable_v_41_35=false, hbv_realizable_v_42_30=true, hbv_realizable_v_43_21=false, hbv_realizable_v_44_22=false, hbv_realizable_v_45_4=false, hbv_realizable_v_46_10=false, hbv_realizable_v_47_41=false]
[L0]  RET   call realizable();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 5 procedures, 22 locations, 36 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 2.2s, OverallIterations: 3, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.4s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 8 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 4 mSDsluCounter, 221 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 169 mSDsCounter, 0 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 72 IncrementalHoareTripleChecker+Invalid, 72 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 0 mSolverCounterUnsat, 52 mSDtfsCounter, 72 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 12 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=22occurred in iteration=0, InterpolantAutomatonStates: 12, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 2 MinimizatonAttempts, 6 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 1.2s InterpolantComputationTime, 48 NumberOfCodeBlocks, 48 NumberOfCodeBlocksAsserted, 3 NumberOfCheckSat, 30 ConstructedInterpolants, 0 QuantifiedInterpolants, 101 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:15,329 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
