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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:11,200 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:11,284 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7a54a4fa-d6ff-4e23-babc-81ee40c7259b/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:11,298 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:11,299 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:11,348 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:11,349 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:11,349 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:11,351 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:11,351 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:11,352 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:11,352 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:11,352 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:11,352 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:11,353 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:11,353 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:11,353 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:11,353 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:11,353 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:11,353 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:11,354 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:11,354 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:11,354 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:11,354 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:11,354 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:11,355 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:11,355 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:11,769 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:11,785 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:11,788 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:11,791 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:11,792 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:11,793 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7a54a4fa-d6ff-4e23-babc-81ee40c7259b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-129.smt2
[2025-04-28 21:21:11,796 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:11,800 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,375 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7a54a4fa-d6ff-4e23-babc-81ee40c7259b/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-129.smt2
[2025-04-28 21:21:12,380 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:12,382 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:12,383 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:12,384 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:12,385 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:12,391 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,456 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,460 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:12,461 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,461 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:12,461 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:12,482 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,482 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,526 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,530 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,535 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,540 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,546 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,548 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,553 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,585 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,586 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:12,586 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:12,586 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:12,587 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,592 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:12,612 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:12,628 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,632 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,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:12,646 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:12,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:12,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:12,646 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:12,646 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:12,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcmainStart__syn given in one single declaration
[2025-04-28 21:21:12,646 INFO  L130     BoogieDeclarations]: Found specification of procedure funcmainStart__syn
[2025-04-28 21:21:12,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcmainStart__syn
[2025-04-28 21:21:12,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:12,647 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:12,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:12,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStartBool__syn given in one single declaration
[2025-04-28 21:21:12,647 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStartBool__syn
[2025-04-28 21:21:12,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStartBool__syn
[2025-04-28 21:21:12,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:12,647 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:12,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:12,790 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:12,792 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:13,221 INFO  L?                        ?]: Removed 24 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:13,221 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:13,235 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:13,235 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:13,235 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:13 BoogieIcfgContainer
[2025-04-28 21:21:13,236 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:13,241 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:13,241 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:13,245 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:13,245 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:13,247 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6066116b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:13, skipping insertion in model container
[2025-04-28 21:21:13,247 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:13,248 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6066116b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:13, skipping insertion in model container
[2025-04-28 21:21:13,248 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:13" (3/3) ...
[2025-04-28 21:21:13,249 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:13,266 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:13,269 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 34 locations, 68 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:13,320 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:13,335 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;@1e97a1a9, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:13,335 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:13,339 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 34 states, 11 states have (on average 1.8181818181818181) internal successors, (20), 17 states have internal predecessors, (20), 16 states have call successors, (16), 5 states have call predecessors, (16), 5 states have return successors, (16), 12 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:13,350 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:13,351 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,351 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,352 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,358 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,359 INFO  L85        PathProgramCache]: Analyzing trace with hash -1252385876, now seen corresponding path program 1 times
[2025-04-28 21:21:13,368 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,368 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1309683487]
[2025-04-28 21:21:13,369 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,369 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,427 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:13,520 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,521 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,521 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:13,521 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-04-28 21:21:13,551 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:13,619 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,619 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,619 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:13,704 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-04-28 21:21:13,706 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-04-28 21:21:13,711 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:13,714 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:13,723 INFO  L422         BasicCegarLoop]: Path program histogram: [1]
[2025-04-28 21:21:13,763 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:13,770 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:13 BoogieIcfgContainer
[2025-04-28 21:21:13,770 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:13,772 INFO  L158              Benchmark]: Toolchain (without parser) took 1389.33ms. Allocated memory is still 234.9MB. Free memory was 148.5MB in the beginning and 188.2MB in the end (delta: -39.7MB). Peak memory consumption was 75.5MB. Max. memory is 33.6GB.
[2025-04-28 21:21:13,772 INFO  L158              Benchmark]: SmtParser took 1.60ms. Allocated memory is still 234.9MB. Free memory was 170.1MB in the beginning and 169.5MB in the end (delta: 587.3kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:13,778 INFO  L158              Benchmark]: ChcToBoogie took 77.20ms. Allocated memory is still 234.9MB. Free memory was 147.9MB in the beginning and 145.5MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:13,778 INFO  L158              Benchmark]: Boogie Preprocessor took 124.08ms. Allocated memory is still 234.9MB. Free memory was 145.5MB in the beginning and 143.2MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:13,779 INFO  L158              Benchmark]: RCFGBuilder took 651.71ms. Allocated memory is still 234.9MB. Free memory was 143.2MB in the beginning and 99.9MB in the end (delta: 43.3MB). Peak memory consumption was 50.3MB. Max. memory is 33.6GB.
[2025-04-28 21:21:13,779 INFO  L158              Benchmark]: TraceAbstraction took 529.75ms. Allocated memory is still 234.9MB. Free memory was 99.3MB in the beginning and 188.2MB in the end (delta: -88.9MB). Peak memory consumption was 25.2MB. Max. memory is 33.6GB.
[2025-04-28 21:21:13,783 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 1.60ms. Allocated memory is still 234.9MB. Free memory was 170.1MB in the beginning and 169.5MB in the end (delta: 587.3kB). There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 77.20ms. Allocated memory is still 234.9MB. Free memory was 147.9MB in the beginning and 145.5MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 124.08ms. Allocated memory is still 234.9MB. Free memory was 145.5MB in the beginning and 143.2MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 651.71ms. Allocated memory is still 234.9MB. Free memory was 143.2MB in the beginning and 99.9MB in the end (delta: 43.3MB). Peak memory consumption was 50.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 529.75ms. Allocated memory is still 234.9MB. Free memory was 99.3MB in the beginning and 188.2MB in the end (delta: -88.9MB). Peak memory consumption was 25.2MB. 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_63_27 && !hbv_realizable_v_55_29) && !((((!hbv_realizable_J1_65 && !hbv_realizable_K1_66) || (!hbv_realizable_I1_67 && hbv_realizable_K1_66)) || !hbv_realizable_E_68) && (hbv_realizable_E_68 || ((hbv_realizable_J1_65 || hbv_realizable_K1_66) && (hbv_realizable_I1_67 || !hbv_realizable_K1_66))))) && !(((hbv_realizable_P_70 && hbv_realizable_Q_71) || hbv_realizable_L_72) && ((!hbv_realizable_P_70 || !hbv_realizable_L_72) || !hbv_realizable_Q_71))) && !hbv_realizable_v_70_6) && !hbv_realizable_v_67_59) && hbv_realizable_v_48_73 == 0) && !!hbv_realizable_v_51_16) && !hbv_realizable_v_61_1) && !hbv_realizable_v_58_49) && !!hbv_realizable_v_50_32) && !hbv_realizable_v_56_28) && !!hbv_realizable_v_60_26) && !hbv_realizable_v_73_30) && !((((!hbv_realizable_W_44 || hbv_realizable_U_45) && (hbv_realizable_V_46 || hbv_realizable_W_44)) || hbv_realizable_J_47) && ((!hbv_realizable_J_47 || (hbv_realizable_W_44 && !hbv_realizable_U_45)) || (!hbv_realizable_W_44 && !hbv_realizable_V_46)))) && !((hbv_realizable_I_53 || ((hbv_realizable_X_50 || !hbv_realizable_Z_51) && (hbv_realizable_Z_51 || hbv_realizable_Y_52))) && (((hbv_realizable_Z_51 && !hbv_realizable_X_50) || (!hbv_realizable_Z_51 && !hbv_realizable_Y_52)) || !hbv_realizable_I_53))) && !!hbv_realizable_v_52_25) && !((((!hbv_realizable_N1_39 && hbv_realizable_P1_40) || (!hbv_realizable_O1_41 && !hbv_realizable_P1_40)) || !hbv_realizable_C_42) && (hbv_realizable_C_42 || ((hbv_realizable_N1_39 || !hbv_realizable_P1_40) && (hbv_realizable_O1_41 || hbv_realizable_P1_40))))) && !hbv_realizable_v_69_43) && !!hbv_realizable_v_49_37) && !((hbv_realizable_B_57 || ((hbv_realizable_R1_54 || hbv_realizable_S1_55) && (!hbv_realizable_S1_55 || hbv_realizable_Q1_56))) && ((!hbv_realizable_B_57 || (!hbv_realizable_S1_55 && !hbv_realizable_R1_54)) || (hbv_realizable_S1_55 && !hbv_realizable_Q1_56)))) && !hbv_realizable_v_54_48) && !hbv_realizable_v_75_38) && !((((!hbv_realizable_T1_11 && hbv_realizable_V1_12) || !hbv_realizable_A_13) || (!hbv_realizable_U1_14 && !hbv_realizable_V1_12)) && (((hbv_realizable_T1_11 || !hbv_realizable_V1_12) && (hbv_realizable_U1_14 || hbv_realizable_V1_12)) || hbv_realizable_A_13))) && !hbv_realizable_v_72_10) && !hbv_realizable_v_53_31) && !((((hbv_realizable_D1_33 || hbv_realizable_E1_34) && (hbv_realizable_C1_35 || !hbv_realizable_E1_34)) || hbv_realizable_G_36) && (((!hbv_realizable_E1_34 && !hbv_realizable_D1_33) || !hbv_realizable_G_36) || (!hbv_realizable_C1_35 && hbv_realizable_E1_34)))) && !(((!hbv_realizable_H_2 || !hbv_realizable_B1_3) || !hbv_realizable_A1_4) && (hbv_realizable_H_2 || (hbv_realizable_A1_4 && hbv_realizable_B1_3)))) && !!hbv_realizable_v_68_64) && !hbv_realizable_v_66_8) && !hbv_realizable_v_71_21) && !hbv_realizable_v_64_9) && !((hbv_realizable_D_24 || (hbv_realizable_L1_22 && hbv_realizable_M1_23)) && ((!hbv_realizable_D_24 || !hbv_realizable_M1_23) || !hbv_realizable_L1_22))) && !hbv_realizable_v_65_7) && !hbv_realizable_v_57_5) && !(((!hbv_realizable_F_19 || (!hbv_realizable_G1_17 && !hbv_realizable_H1_18)) || (hbv_realizable_H1_18 && !hbv_realizable_F1_20)) && (((hbv_realizable_G1_17 || hbv_realizable_H1_18) && (!hbv_realizable_H1_18 || hbv_realizable_F1_20)) || hbv_realizable_F_19))) && !hbv_realizable_v_59_69) && !hbv_realizable_v_74_15) && !((((!hbv_realizable_R_60 && hbv_realizable_T_61) || !hbv_realizable_K_62) || (!hbv_realizable_T_61 && !hbv_realizable_S_63)) && (((hbv_realizable_S_63 || hbv_realizable_T_61) && (!hbv_realizable_T_61 || hbv_realizable_R_60)) || hbv_realizable_K_62))) && !hbv_realizable_v_62_58;
      VAL   [hbv_realizable_A_13=false, hbv_realizable_B1_3=false, hbv_realizable_B_57=false, hbv_realizable_C_42=false, hbv_realizable_D_24=false, hbv_realizable_E1_34=false, hbv_realizable_E_68=false, hbv_realizable_F_19=false, hbv_realizable_G_36=false, hbv_realizable_H1_18=false, hbv_realizable_H_2=false, hbv_realizable_I_53=false, hbv_realizable_J_47=false, hbv_realizable_K1_66=false, hbv_realizable_K_62=false, hbv_realizable_L_72=false, hbv_realizable_M1_23=false, hbv_realizable_P1_40=false, hbv_realizable_Q_71=false, hbv_realizable_S1_55=false, hbv_realizable_T_61=false, hbv_realizable_V1_12=false, hbv_realizable_W_44=false, hbv_realizable_Z_51=false, hbv_realizable_v_48_73=0, hbv_realizable_v_49_37=true, hbv_realizable_v_50_32=true, hbv_realizable_v_51_16=true, hbv_realizable_v_52_25=true, hbv_realizable_v_53_31=false, hbv_realizable_v_54_48=false, hbv_realizable_v_55_29=false, hbv_realizable_v_56_28=false, hbv_realizable_v_57_5=false, hbv_realizable_v_58_49=false, hbv_realizable_v_59_69=false, hbv_realizable_v_60_26=true, hbv_realizable_v_61_1=false, hbv_realizable_v_62_58=false, hbv_realizable_v_63_27=false, hbv_realizable_v_64_9=false, hbv_realizable_v_65_7=false, hbv_realizable_v_66_8=false, hbv_realizable_v_67_59=false, hbv_realizable_v_68_64=true, hbv_realizable_v_69_43=false, hbv_realizable_v_70_6=false, hbv_realizable_v_71_21=false, hbv_realizable_v_72_10=false, hbv_realizable_v_73_30=false, hbv_realizable_v_74_15=false, hbv_realizable_v_75_38=false]
[L0]  CALL  call funcmainStart__syn(hbv_realizable_M_74, hbv_realizable_v_48_73, hbv_realizable_v_49_37, hbv_realizable_v_50_32, hbv_realizable_v_51_16, hbv_realizable_v_52_25, hbv_realizable_v_53_31, hbv_realizable_v_54_48, hbv_realizable_v_55_29, hbv_realizable_v_56_28, hbv_realizable_v_57_5, hbv_realizable_v_58_49, hbv_realizable_v_59_69, hbv_realizable_v_60_26, hbv_realizable_v_61_1, hbv_realizable_v_62_58, hbv_realizable_v_63_27, hbv_realizable_v_64_9, hbv_realizable_v_65_7, hbv_realizable_v_66_8, hbv_realizable_v_67_59, hbv_realizable_v_68_64, hbv_realizable_v_69_43, hbv_realizable_v_70_6, hbv_realizable_v_71_21, hbv_realizable_v_72_10, hbv_realizable_v_73_30, hbv_realizable_v_74_15, hbv_realizable_v_75_38, hbv_realizable_N_75, hbv_realizable_O_76, hbv_realizable_L_72, hbv_realizable_Q_71, hbv_realizable_K_62, hbv_realizable_T_61, hbv_realizable_J_47, hbv_realizable_W_44, hbv_realizable_I_53, hbv_realizable_Z_51, hbv_realizable_H_2, hbv_realizable_B1_3, hbv_realizable_G_36, hbv_realizable_E1_34, hbv_realizable_F_19, hbv_realizable_H1_18, hbv_realizable_E_68, hbv_realizable_K1_66, hbv_realizable_D_24, hbv_realizable_M1_23, hbv_realizable_C_42, hbv_realizable_P1_40, hbv_realizable_B_57, hbv_realizable_S1_55, hbv_realizable_A_13, hbv_realizable_V1_12);
      VAL   [hhv_funcmainStart__syn_B1_14=false, hhv_funcmainStart__syn_C1_15=false, hhv_funcmainStart__syn_C_48=false, hhv_funcmainStart__syn_D1_16=false, hhv_funcmainStart__syn_D_47=false, hhv_funcmainStart__syn_E1_17=false, hhv_funcmainStart__syn_E_40=false, hhv_funcmainStart__syn_F1_18=false, hhv_funcmainStart__syn_F_39=false, hhv_funcmainStart__syn_G1_19=false, hhv_funcmainStart__syn_G_32=false, hhv_funcmainStart__syn_H1_20=false, hhv_funcmainStart__syn_H_31=false, hhv_funcmainStart__syn_J1_21=true, hhv_funcmainStart__syn_J_1=0, hhv_funcmainStart__syn_K1_4=true, hhv_funcmainStart__syn_L_30=2, hhv_funcmainStart__syn_M1_22=false, hhv_funcmainStart__syn_N1_23=false, hhv_funcmainStart__syn_N_5=true, hhv_funcmainStart__syn_O1_24=false, hhv_funcmainStart__syn_O_2=true, hhv_funcmainStart__syn_P1_25=false, hhv_funcmainStart__syn_Q1_26=false, hhv_funcmainStart__syn_Q_6=false, hhv_funcmainStart__syn_R1_27=false, hhv_funcmainStart__syn_R_7=false, hhv_funcmainStart__syn_S1_28=false, hhv_funcmainStart__syn_S_8=false, hhv_funcmainStart__syn_T_9=false, hhv_funcmainStart__syn_U_10=false, hhv_funcmainStart__syn_V_11=false, hhv_funcmainStart__syn_W_12=false, hhv_funcmainStart__syn_Y_13=true, hhv_funcmainStart__syn_Z_3=true, hhv_funcmainStart__syn_v_45_33=false, hhv_funcmainStart__syn_v_46_34=false, hhv_funcmainStart__syn_v_47_35=false, hhv_funcmainStart__syn_v_48_36=false, hhv_funcmainStart__syn_v_49_37=false, hhv_funcmainStart__syn_v_50_38=false, hhv_funcmainStart__syn_v_51_41=false, hhv_funcmainStart__syn_v_52_42=false, hhv_funcmainStart__syn_v_53_43=false, hhv_funcmainStart__syn_v_54_44=false, hhv_funcmainStart__syn_v_55_45=false, hhv_funcmainStart__syn_v_56_46=false, hhv_funcmainStart__syn_v_57_49=false, hhv_funcmainStart__syn_v_58_50=false, hhv_funcmainStart__syn_v_59_51=false, hhv_funcmainStart__syn_v_60_52=false, hhv_funcmainStart__syn_v_61_53=false, hhv_funcmainStart__syn_v_62_54=false]
[L0]        assume ((((((((((((((((((((((((!((!hhv_funcmainStart__syn_G1_19 || !hhv_funcmainStart__syn_v_55_45) && (hhv_funcmainStart__syn_G1_19 || hhv_funcmainStart__syn_v_55_45)) && hbv_funcmainStart__syn_B_2 == hhv_funcmainStart__syn_I_0[hhv_funcmainStart__syn_J_1 := 0]) && !((!hhv_funcmainStart__syn_S1_28 || !hhv_funcmainStart__syn_v_62_54) && (hhv_funcmainStart__syn_S1_28 || hhv_funcmainStart__syn_v_62_54))) && !((!hhv_funcmainStart__syn_v_61_53 || !hhv_funcmainStart__syn_R1_27) && (hhv_funcmainStart__syn_R1_27 || hhv_funcmainStart__syn_v_61_53))) && hhv_funcmainStart__syn_J_1 + 1 == hbv_funcmainStart__syn_A_6) && !((hhv_funcmainStart__syn_D_47 || ((hhv_funcmainStart__syn_J1_21 || hhv_funcmainStart__syn_K1_4) && (hbv_funcmainStart__syn_I1_3 || !hhv_funcmainStart__syn_K1_4))) && (((!hhv_funcmainStart__syn_J1_21 && !hhv_funcmainStart__syn_K1_4) || (!hbv_funcmainStart__syn_I1_3 && hhv_funcmainStart__syn_K1_4)) || !hhv_funcmainStart__syn_D_47))) && !((hhv_funcmainStart__syn_T_9 || hhv_funcmainStart__syn_v_47_35) && (!hhv_funcmainStart__syn_v_47_35 || !hhv_funcmainStart__syn_T_9))) && !((!hhv_funcmainStart__syn_v_54_44 || !hhv_funcmainStart__syn_F1_18) && (hhv_funcmainStart__syn_F1_18 || hhv_funcmainStart__syn_v_54_44))) && !((!hhv_funcmainStart__syn_v_52_42 || !hhv_funcmainStart__syn_D1_16) && (hhv_funcmainStart__syn_D1_16 || hhv_funcmainStart__syn_v_52_42))) && !((hhv_funcmainStart__syn_N1_23 || hhv_funcmainStart__syn_v_57_49) && (!hhv_funcmainStart__syn_N1_23 || !hhv_funcmainStart__syn_v_57_49))) && !((!hhv_funcmainStart__syn_C1_15 || !hhv_funcmainStart__syn_v_51_41) && (hhv_funcmainStart__syn_C1_15 || hhv_funcmainStart__syn_v_51_41))) && !(((!hhv_funcmainStart__syn_H_31 || (!hbv_funcmainStart__syn_M_4 && hhv_funcmainStart__syn_O_2)) || (!hhv_funcmainStart__syn_O_2 && !hhv_funcmainStart__syn_N_5)) && (((hhv_funcmainStart__syn_N_5 || hhv_funcmainStart__syn_O_2) && (!hhv_funcmainStart__syn_O_2 || hbv_funcmainStart__syn_M_4)) || hhv_funcmainStart__syn_H_31))) && !((hhv_funcmainStart__syn_P1_25 || hhv_funcmainStart__syn_v_59_51) && (!hhv_funcmainStart__syn_v_59_51 || !hhv_funcmainStart__syn_P1_25))) && !((((hhv_funcmainStart__syn_Z_3 && !hbv_funcmainStart__syn_A1_5) || (!hhv_funcmainStart__syn_B1_14 && !hhv_funcmainStart__syn_Z_3)) || !hhv_funcmainStart__syn_E_40) && (((hhv_funcmainStart__syn_B1_14 || hhv_funcmainStart__syn_Z_3) && (hbv_funcmainStart__syn_A1_5 || !hhv_funcmainStart__syn_Z_3)) || hhv_funcmainStart__syn_E_40))) && !((hhv_funcmainStart__syn_U_10 || hhv_funcmainStart__syn_v_48_36) && (!hhv_funcmainStart__syn_v_48_36 || !hhv_funcmainStart__syn_U_10))) && !((!hhv_funcmainStart__syn_v_53_43 || !hhv_funcmainStart__syn_E1_17) && (hhv_funcmainStart__syn_E1_17 || hhv_funcmainStart__syn_v_53_43))) && !((hhv_funcmainStart__syn_G_32 || ((!hhv_funcmainStart__syn_O_2 || hbv_funcmainStart__syn_P_1) && (hhv_funcmainStart__syn_O_2 || hhv_funcmainStart__syn_Q_6))) && ((!hhv_funcmainStart__syn_G_32 || (!hhv_funcmainStart__syn_O_2 && !hhv_funcmainStart__syn_Q_6)) || (!hbv_funcmainStart__syn_P_1 && hhv_funcmainStart__syn_O_2)))) && !((!hhv_funcmainStart__syn_S_8 || !hhv_funcmainStart__syn_v_46_34) && (hhv_funcmainStart__syn_S_8 || hhv_funcmainStart__syn_v_46_34))) && !((!hhv_funcmainStart__syn_W_12 || !hhv_funcmainStart__syn_v_50_38) && (hhv_funcmainStart__syn_W_12 || hhv_funcmainStart__syn_v_50_38))) && !((hhv_funcmainStart__syn_F_39 || ((hbv_funcmainStart__syn_X_8 || !hhv_funcmainStart__syn_Z_3) && (hhv_funcmainStart__syn_Z_3 || hhv_funcmainStart__syn_Y_13))) && (((hhv_funcmainStart__syn_Z_3 && !hbv_funcmainStart__syn_X_8) || !hhv_funcmainStart__syn_F_39) || (!hhv_funcmainStart__syn_Z_3 && !hhv_funcmainStart__syn_Y_13)))) && !((!hhv_funcmainStart__syn_v_49_37 || !hhv_funcmainStart__syn_V_11) && (hhv_funcmainStart__syn_V_11 || hhv_funcmainStart__syn_v_49_37))) && !((!hhv_funcmainStart__syn_O1_24 || !hhv_funcmainStart__syn_v_58_50) && (hhv_funcmainStart__syn_O1_24 || hhv_funcmainStart__syn_v_58_50))) && !((!hhv_funcmainStart__syn_R_7 || !hhv_funcmainStart__syn_v_45_33) && (hhv_funcmainStart__syn_R_7 || hhv_funcmainStart__syn_v_45_33))) && !((hhv_funcmainStart__syn_Q1_26 || hhv_funcmainStart__syn_v_60_52) && (!hhv_funcmainStart__syn_v_60_52 || !hhv_funcmainStart__syn_Q1_26))) && !((!hhv_funcmainStart__syn_H1_20 || !hhv_funcmainStart__syn_v_56_46) && (hhv_funcmainStart__syn_H1_20 || hhv_funcmainStart__syn_v_56_46))) && !((((hhv_funcmainStart__syn_K1_4 && !hbv_funcmainStart__syn_L1_7) || (!hhv_funcmainStart__syn_K1_4 && !hhv_funcmainStart__syn_M1_22)) || !hhv_funcmainStart__syn_C_48) && (((hhv_funcmainStart__syn_K1_4 || hhv_funcmainStart__syn_M1_22) && (hbv_funcmainStart__syn_L1_7 || !hhv_funcmainStart__syn_K1_4)) || hhv_funcmainStart__syn_C_48));
      VAL   [hbv_funcmainStart__syn_A1_5=false, hbv_funcmainStart__syn_A_6=1, hbv_funcmainStart__syn_I1_3=false, hbv_funcmainStart__syn_L1_7=false, hbv_funcmainStart__syn_M_4=false, hbv_funcmainStart__syn_P_1=false, hbv_funcmainStart__syn_X_8=false, hhv_funcmainStart__syn_B1_14=false, hhv_funcmainStart__syn_C1_15=false, hhv_funcmainStart__syn_C_48=false, hhv_funcmainStart__syn_D1_16=false, hhv_funcmainStart__syn_D_47=false, hhv_funcmainStart__syn_E1_17=false, hhv_funcmainStart__syn_E_40=false, hhv_funcmainStart__syn_F1_18=false, hhv_funcmainStart__syn_F_39=false, hhv_funcmainStart__syn_G1_19=false, hhv_funcmainStart__syn_G_32=false, hhv_funcmainStart__syn_H1_20=false, hhv_funcmainStart__syn_H_31=false, hhv_funcmainStart__syn_J1_21=true, hhv_funcmainStart__syn_J_1=0, hhv_funcmainStart__syn_K1_4=true, hhv_funcmainStart__syn_L_30=2, hhv_funcmainStart__syn_M1_22=false, hhv_funcmainStart__syn_N1_23=false, hhv_funcmainStart__syn_N_5=true, hhv_funcmainStart__syn_O1_24=false, hhv_funcmainStart__syn_O_2=true, hhv_funcmainStart__syn_P1_25=false, hhv_funcmainStart__syn_Q1_26=false, hhv_funcmainStart__syn_Q_6=false, hhv_funcmainStart__syn_R1_27=false, hhv_funcmainStart__syn_R_7=false, hhv_funcmainStart__syn_S1_28=false, hhv_funcmainStart__syn_S_8=false, hhv_funcmainStart__syn_T_9=false, hhv_funcmainStart__syn_U_10=false, hhv_funcmainStart__syn_V_11=false, hhv_funcmainStart__syn_W_12=false, hhv_funcmainStart__syn_Y_13=true, hhv_funcmainStart__syn_Z_3=true, hhv_funcmainStart__syn_v_45_33=false, hhv_funcmainStart__syn_v_46_34=false, hhv_funcmainStart__syn_v_47_35=false, hhv_funcmainStart__syn_v_48_36=false, hhv_funcmainStart__syn_v_49_37=false, hhv_funcmainStart__syn_v_50_38=false, hhv_funcmainStart__syn_v_51_41=false, hhv_funcmainStart__syn_v_52_42=false, hhv_funcmainStart__syn_v_53_43=false, hhv_funcmainStart__syn_v_54_44=false, hhv_funcmainStart__syn_v_55_45=false, hhv_funcmainStart__syn_v_56_46=false, hhv_funcmainStart__syn_v_57_49=false, hhv_funcmainStart__syn_v_58_50=false, hhv_funcmainStart__syn_v_59_51=false, hhv_funcmainStart__syn_v_60_52=false, hhv_funcmainStart__syn_v_61_53=false, hhv_funcmainStart__syn_v_62_54=false]
[L0]  CALL  call funcStart__syn(hbv_funcmainStart__syn_B_2, hbv_funcmainStart__syn_A_6, hhv_funcmainStart__syn_O_2, hhv_funcmainStart__syn_Z_3, hhv_funcmainStart__syn_K1_4, hhv_funcmainStart__syn_N_5, hhv_funcmainStart__syn_Q_6, hhv_funcmainStart__syn_R_7, hhv_funcmainStart__syn_S_8, hhv_funcmainStart__syn_T_9, hhv_funcmainStart__syn_U_10, hhv_funcmainStart__syn_V_11, hhv_funcmainStart__syn_W_12, hhv_funcmainStart__syn_Y_13, hhv_funcmainStart__syn_B1_14, hhv_funcmainStart__syn_C1_15, hhv_funcmainStart__syn_D1_16, hhv_funcmainStart__syn_E1_17, hhv_funcmainStart__syn_F1_18, hhv_funcmainStart__syn_G1_19, hhv_funcmainStart__syn_H1_20, hhv_funcmainStart__syn_J1_21, hhv_funcmainStart__syn_M1_22, hhv_funcmainStart__syn_N1_23, hhv_funcmainStart__syn_O1_24, hhv_funcmainStart__syn_P1_25, hhv_funcmainStart__syn_Q1_26, hhv_funcmainStart__syn_R1_27, hhv_funcmainStart__syn_S1_28, hhv_funcmainStart__syn_K_29, hhv_funcmainStart__syn_L_30, hbv_funcmainStart__syn_M_4, hbv_funcmainStart__syn_P_1, hbv_funcmainStart__syn_X_8, hbv_funcmainStart__syn_A1_5, hbv_funcmainStart__syn_I1_3, hbv_funcmainStart__syn_L1_7);
      VAL   [hhv_funcStart__syn_A1_26=false, hhv_funcStart__syn_B1_27=false, hhv_funcStart__syn_B_1=1, hhv_funcStart__syn_C1_28=false, hhv_funcStart__syn_C_2=true, hhv_funcStart__syn_D_3=true, hhv_funcStart__syn_E1_30=2, hhv_funcStart__syn_E_4=true, hhv_funcStart__syn_F_5=true, hhv_funcStart__syn_G_6=false, hhv_funcStart__syn_H_7=false, hhv_funcStart__syn_I_8=false, hhv_funcStart__syn_J_9=false, hhv_funcStart__syn_K_10=false, hhv_funcStart__syn_L_11=false, hhv_funcStart__syn_M_12=false, hhv_funcStart__syn_N_13=true, hhv_funcStart__syn_O_14=false, hhv_funcStart__syn_P_15=false, hhv_funcStart__syn_Q_16=false, hhv_funcStart__syn_R_17=false, hhv_funcStart__syn_S_18=false, hhv_funcStart__syn_T_19=false, hhv_funcStart__syn_U_20=false, hhv_funcStart__syn_V_21=true, hhv_funcStart__syn_W_22=false, hhv_funcStart__syn_X_23=false, hhv_funcStart__syn_Y_24=false, hhv_funcStart__syn_Z_25=false, hhv_funcStart__syn_v_31_31=false, hhv_funcStart__syn_v_32_32=false, hhv_funcStart__syn_v_33_33=false, hhv_funcStart__syn_v_34_34=false, hhv_funcStart__syn_v_35_35=false, hhv_funcStart__syn_v_36_36=false]
[L0]        assume ((((((!((hhv_funcStart__syn_B1_27 || hhv_funcStart__syn_v_35_35) && (!hhv_funcStart__syn_v_35_35 || !hhv_funcStart__syn_B1_27)) && !((!hhv_funcStart__syn_L_11 || !hhv_funcStart__syn_v_31_31) && (hhv_funcStart__syn_L_11 || hhv_funcStart__syn_v_31_31))) && hhv_funcStart__syn_B_1 + 1 == hhv_funcStart__syn_E1_30) && !((hhv_funcStart__syn_C1_28 || hhv_funcStart__syn_v_36_36) && (!hhv_funcStart__syn_v_36_36 || !hhv_funcStart__syn_C1_28))) && hhv_funcStart__syn_D1_29 == hhv_funcStart__syn_A_0[hhv_funcStart__syn_B_1 := 4]) && !((hhv_funcStart__syn_M_12 || hhv_funcStart__syn_v_32_32) && (!hhv_funcStart__syn_v_32_32 || !hhv_funcStart__syn_M_12))) && !((!hhv_funcStart__syn_T_19 || !hhv_funcStart__syn_v_33_33) && (hhv_funcStart__syn_T_19 || hhv_funcStart__syn_v_33_33))) && !((hhv_funcStart__syn_U_20 || hhv_funcStart__syn_v_34_34) && (!hhv_funcStart__syn_U_20 || !hhv_funcStart__syn_v_34_34));
      VAL   [hhv_funcStart__syn_A1_26=false, hhv_funcStart__syn_B1_27=false, hhv_funcStart__syn_B_1=1, hhv_funcStart__syn_C1_28=false, hhv_funcStart__syn_C_2=true, hhv_funcStart__syn_D_3=true, hhv_funcStart__syn_E1_30=2, hhv_funcStart__syn_E_4=true, hhv_funcStart__syn_F_5=true, hhv_funcStart__syn_G_6=false, hhv_funcStart__syn_H_7=false, hhv_funcStart__syn_I_8=false, hhv_funcStart__syn_J_9=false, hhv_funcStart__syn_K_10=false, hhv_funcStart__syn_L_11=false, hhv_funcStart__syn_M_12=false, hhv_funcStart__syn_N_13=true, hhv_funcStart__syn_O_14=false, hhv_funcStart__syn_P_15=false, hhv_funcStart__syn_Q_16=false, hhv_funcStart__syn_R_17=false, hhv_funcStart__syn_S_18=false, hhv_funcStart__syn_T_19=false, hhv_funcStart__syn_U_20=false, hhv_funcStart__syn_V_21=true, hhv_funcStart__syn_W_22=false, hhv_funcStart__syn_X_23=false, hhv_funcStart__syn_Y_24=false, hhv_funcStart__syn_Z_25=false, hhv_funcStart__syn_v_31_31=false, hhv_funcStart__syn_v_32_32=false, hhv_funcStart__syn_v_33_33=false, hhv_funcStart__syn_v_34_34=false, hhv_funcStart__syn_v_35_35=false, hhv_funcStart__syn_v_36_36=false]
[L0]  RET   call funcStart__syn(hbv_funcmainStart__syn_B_2, hbv_funcmainStart__syn_A_6, hhv_funcmainStart__syn_O_2, hhv_funcmainStart__syn_Z_3, hhv_funcmainStart__syn_K1_4, hhv_funcmainStart__syn_N_5, hhv_funcmainStart__syn_Q_6, hhv_funcmainStart__syn_R_7, hhv_funcmainStart__syn_S_8, hhv_funcmainStart__syn_T_9, hhv_funcmainStart__syn_U_10, hhv_funcmainStart__syn_V_11, hhv_funcmainStart__syn_W_12, hhv_funcmainStart__syn_Y_13, hhv_funcmainStart__syn_B1_14, hhv_funcmainStart__syn_C1_15, hhv_funcmainStart__syn_D1_16, hhv_funcmainStart__syn_E1_17, hhv_funcmainStart__syn_F1_18, hhv_funcmainStart__syn_G1_19, hhv_funcmainStart__syn_H1_20, hhv_funcmainStart__syn_J1_21, hhv_funcmainStart__syn_M1_22, hhv_funcmainStart__syn_N1_23, hhv_funcmainStart__syn_O1_24, hhv_funcmainStart__syn_P1_25, hhv_funcmainStart__syn_Q1_26, hhv_funcmainStart__syn_R1_27, hhv_funcmainStart__syn_S1_28, hhv_funcmainStart__syn_K_29, hhv_funcmainStart__syn_L_30, hbv_funcmainStart__syn_M_4, hbv_funcmainStart__syn_P_1, hbv_funcmainStart__syn_X_8, hbv_funcmainStart__syn_A1_5, hbv_funcmainStart__syn_I1_3, hbv_funcmainStart__syn_L1_7);
      VAL   [hbv_funcmainStart__syn_A1_5=false, hbv_funcmainStart__syn_A_6=1, hbv_funcmainStart__syn_I1_3=false, hbv_funcmainStart__syn_L1_7=false, hbv_funcmainStart__syn_M_4=false, hbv_funcmainStart__syn_P_1=false, hbv_funcmainStart__syn_X_8=false, hhv_funcmainStart__syn_B1_14=false, hhv_funcmainStart__syn_C1_15=false, hhv_funcmainStart__syn_C_48=false, hhv_funcmainStart__syn_D1_16=false, hhv_funcmainStart__syn_D_47=false, hhv_funcmainStart__syn_E1_17=false, hhv_funcmainStart__syn_E_40=false, hhv_funcmainStart__syn_F1_18=false, hhv_funcmainStart__syn_F_39=false, hhv_funcmainStart__syn_G1_19=false, hhv_funcmainStart__syn_G_32=false, hhv_funcmainStart__syn_H1_20=false, hhv_funcmainStart__syn_H_31=false, hhv_funcmainStart__syn_J1_21=true, hhv_funcmainStart__syn_J_1=0, hhv_funcmainStart__syn_K1_4=true, hhv_funcmainStart__syn_L_30=2, hhv_funcmainStart__syn_M1_22=false, hhv_funcmainStart__syn_N1_23=false, hhv_funcmainStart__syn_N_5=true, hhv_funcmainStart__syn_O1_24=false, hhv_funcmainStart__syn_O_2=true, hhv_funcmainStart__syn_P1_25=false, hhv_funcmainStart__syn_Q1_26=false, hhv_funcmainStart__syn_Q_6=false, hhv_funcmainStart__syn_R1_27=false, hhv_funcmainStart__syn_R_7=false, hhv_funcmainStart__syn_S1_28=false, hhv_funcmainStart__syn_S_8=false, hhv_funcmainStart__syn_T_9=false, hhv_funcmainStart__syn_U_10=false, hhv_funcmainStart__syn_V_11=false, hhv_funcmainStart__syn_W_12=false, hhv_funcmainStart__syn_Y_13=true, hhv_funcmainStart__syn_Z_3=true, hhv_funcmainStart__syn_v_45_33=false, hhv_funcmainStart__syn_v_46_34=false, hhv_funcmainStart__syn_v_47_35=false, hhv_funcmainStart__syn_v_48_36=false, hhv_funcmainStart__syn_v_49_37=false, hhv_funcmainStart__syn_v_50_38=false, hhv_funcmainStart__syn_v_51_41=false, hhv_funcmainStart__syn_v_52_42=false, hhv_funcmainStart__syn_v_53_43=false, hhv_funcmainStart__syn_v_54_44=false, hhv_funcmainStart__syn_v_55_45=false, hhv_funcmainStart__syn_v_56_46=false, hhv_funcmainStart__syn_v_57_49=false, hhv_funcmainStart__syn_v_58_50=false, hhv_funcmainStart__syn_v_59_51=false, hhv_funcmainStart__syn_v_60_52=false, hhv_funcmainStart__syn_v_61_53=false, hhv_funcmainStart__syn_v_62_54=false]
[L0]  RET   call funcmainStart__syn(hbv_realizable_M_74, hbv_realizable_v_48_73, hbv_realizable_v_49_37, hbv_realizable_v_50_32, hbv_realizable_v_51_16, hbv_realizable_v_52_25, hbv_realizable_v_53_31, hbv_realizable_v_54_48, hbv_realizable_v_55_29, hbv_realizable_v_56_28, hbv_realizable_v_57_5, hbv_realizable_v_58_49, hbv_realizable_v_59_69, hbv_realizable_v_60_26, hbv_realizable_v_61_1, hbv_realizable_v_62_58, hbv_realizable_v_63_27, hbv_realizable_v_64_9, hbv_realizable_v_65_7, hbv_realizable_v_66_8, hbv_realizable_v_67_59, hbv_realizable_v_68_64, hbv_realizable_v_69_43, hbv_realizable_v_70_6, hbv_realizable_v_71_21, hbv_realizable_v_72_10, hbv_realizable_v_73_30, hbv_realizable_v_74_15, hbv_realizable_v_75_38, hbv_realizable_N_75, hbv_realizable_O_76, hbv_realizable_L_72, hbv_realizable_Q_71, hbv_realizable_K_62, hbv_realizable_T_61, hbv_realizable_J_47, hbv_realizable_W_44, hbv_realizable_I_53, hbv_realizable_Z_51, hbv_realizable_H_2, hbv_realizable_B1_3, hbv_realizable_G_36, hbv_realizable_E1_34, hbv_realizable_F_19, hbv_realizable_H1_18, hbv_realizable_E_68, hbv_realizable_K1_66, hbv_realizable_D_24, hbv_realizable_M1_23, hbv_realizable_C_42, hbv_realizable_P1_40, hbv_realizable_B_57, hbv_realizable_S1_55, hbv_realizable_A_13, hbv_realizable_V1_12);
      VAL   [hbv_realizable_A_13=false, hbv_realizable_B1_3=false, hbv_realizable_B_57=false, hbv_realizable_C_42=false, hbv_realizable_D_24=false, hbv_realizable_E1_34=false, hbv_realizable_E_68=false, hbv_realizable_F_19=false, hbv_realizable_G_36=false, hbv_realizable_H1_18=false, hbv_realizable_H_2=false, hbv_realizable_I_53=false, hbv_realizable_J_47=false, hbv_realizable_K1_66=false, hbv_realizable_K_62=false, hbv_realizable_L_72=false, hbv_realizable_M1_23=false, hbv_realizable_O_76=2, hbv_realizable_P1_40=false, hbv_realizable_Q_71=false, hbv_realizable_S1_55=false, hbv_realizable_T_61=false, hbv_realizable_V1_12=false, hbv_realizable_W_44=false, hbv_realizable_Z_51=false, hbv_realizable_v_48_73=0, hbv_realizable_v_49_37=true, hbv_realizable_v_50_32=true, hbv_realizable_v_51_16=true, hbv_realizable_v_52_25=true, hbv_realizable_v_53_31=false, hbv_realizable_v_54_48=false, hbv_realizable_v_55_29=false, hbv_realizable_v_56_28=false, hbv_realizable_v_57_5=false, hbv_realizable_v_58_49=false, hbv_realizable_v_59_69=false, hbv_realizable_v_60_26=true, hbv_realizable_v_61_1=false, hbv_realizable_v_62_58=false, hbv_realizable_v_63_27=false, hbv_realizable_v_64_9=false, hbv_realizable_v_65_7=false, hbv_realizable_v_66_8=false, hbv_realizable_v_67_59=false, hbv_realizable_v_68_64=true, hbv_realizable_v_69_43=false, hbv_realizable_v_70_6=false, hbv_realizable_v_71_21=false, hbv_realizable_v_72_10=false, hbv_realizable_v_73_30=false, hbv_realizable_v_74_15=false, hbv_realizable_v_75_38=false]
[L0]  RET   call realizable();
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 6 procedures, 34 locations, 68 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 0.4s, OverallIterations: 1, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.0s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: , PredicateUnifierStatistics: No data available, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=34occurred in iteration=0, InterpolantAutomatonStates: 0, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: No data available, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.0s InterpolantComputationTime, 16 NumberOfCodeBlocks, 16 NumberOfCodeBlocksAsserted, 1 NumberOfCheckSat, 0 ConstructedInterpolants, 0 QuantifiedInterpolants, 0 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 0 InterpolantComputations, 0 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:13,807 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...
unsat
