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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:19,143 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:19,206 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_36ce54cd-c1db-42dc-a88a-3b65016bda51/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:19,210 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:19,210 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:19,249 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:19,249 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:19,249 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:19,250 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:19,250 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:19,250 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:19,250 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:19,250 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:19,251 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:19,251 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:19,251 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:19,251 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:19,251 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:19,251 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:19,252 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:19,252 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:19,252 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:19,252 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:19,252 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:19,252 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:19,253 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:19,253 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:19,632 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:19,644 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:19,647 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:19,648 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:19,649 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:19,650 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_36ce54cd-c1db-42dc-a88a-3b65016bda51/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-191.smt2
[2025-04-28 21:21:19,652 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:19,656 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:19,865 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_36ce54cd-c1db-42dc-a88a-3b65016bda51/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-191.smt2
[2025-04-28 21:21:19,869 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:19,870 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:19,871 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:19,871 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:19,871 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:19,874 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,903 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19 Unit
[2025-04-28 21:21:19,903 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:19,905 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,906 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:19,906 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:19,924 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,925 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,958 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,960 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,963 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,964 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,967 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,969 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,974 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,993 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,994 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:19,994 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:19,994 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:19,995 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:20,000 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:20,018 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,036 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:20,039 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:20,050 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:20,050 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:20,051 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:20,051 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main37 given in one single declaration
[2025-04-28 21:21:20,051 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main37
[2025-04-28 21:21:20,051 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main37
[2025-04-28 21:21:20,051 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main31 given in one single declaration
[2025-04-28 21:21:20,051 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main31
[2025-04-28 21:21:20,051 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main31
[2025-04-28 21:21:20,051 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main25 given in one single declaration
[2025-04-28 21:21:20,051 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main25
[2025-04-28 21:21:20,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main25
[2025-04-28 21:21:20,052 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main14 given in one single declaration
[2025-04-28 21:21:20,052 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main14
[2025-04-28 21:21:20,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main14
[2025-04-28 21:21:20,052 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main8 given in one single declaration
[2025-04-28 21:21:20,052 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main8
[2025-04-28 21:21:20,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main8
[2025-04-28 21:21:20,052 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main3 given in one single declaration
[2025-04-28 21:21:20,052 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main3
[2025-04-28 21:21:20,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main3
[2025-04-28 21:21:20,053 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:20,053 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:20,053 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:20,126 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:20,129 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:20,305 INFO  L?                        ?]: Removed 9 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:20,306 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:20,326 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:20,327 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:20,327 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:20 BoogieIcfgContainer
[2025-04-28 21:21:20,328 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:20,331 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:20,331 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:20,338 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:20,338 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/3) ...
[2025-04-28 21:21:20,339 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5b5db1ab and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:20, skipping insertion in model container
[2025-04-28 21:21:20,339 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (2/3) ...
[2025-04-28 21:21:20,339 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5b5db1ab and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:20, skipping insertion in model container
[2025-04-28 21:21:20,339 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:20" (3/3) ...
[2025-04-28 21:21:20,343 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:20,362 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:20,366 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 35 locations, 53 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:20,425 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:20,440 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;@504fe95a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:20,440 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:20,445 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 35 states, 15 states have (on average 1.3333333333333333) internal successors, (20), 20 states have internal predecessors, (20), 11 states have call successors, (11), 7 states have call predecessors, (11), 7 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:21:20,455 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:20,455 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,456 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,456 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,462 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,463 INFO  L85        PathProgramCache]: Analyzing trace with hash 1657336010, now seen corresponding path program 1 times
[2025-04-28 21:21:20,472 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,473 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [630327687]
[2025-04-28 21:21:20,473 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,474 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,509 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:20,535 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:20,536 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,536 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,107 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:21,109 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,110 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [630327687]
[2025-04-28 21:21:21,111 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [630327687] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,111 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,117 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:21,119 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1279625833]
[2025-04-28 21:21:21,120 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,124 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:21,124 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,162 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:21,163 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:21,165 INFO  L87              Difference]: Start difference. First operand  has 35 states, 15 states have (on average 1.3333333333333333) internal successors, (20), 20 states have internal predecessors, (20), 11 states have call successors, (11), 7 states have call predecessors, (11), 7 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11) Second operand  has 9 states, 7 states have (on average 2.0) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:21,429 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,432 INFO  L93              Difference]: Finished difference Result 45 states and 56 transitions.
[2025-04-28 21:21:21,433 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:21,434 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 2.0) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:21,435 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,443 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:21,444 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:21,446 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:21,453 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 3 mSDsluCounter, 203 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 235 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,457 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 235 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:21,497 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:21,553 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 41.
[2025-04-28 21:21:21,554 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 18 states have (on average 1.2222222222222223) internal successors, (22), 22 states have internal predecessors, (22), 11 states have call successors, (11), 7 states have call predecessors, (11), 11 states have return successors, (18), 11 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:21,562 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 51 transitions.
[2025-04-28 21:21:21,564 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 51 transitions. Word has length 28
[2025-04-28 21:21:21,564 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,564 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 51 transitions.
[2025-04-28 21:21:21,564 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 2.0) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:21,565 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 51 transitions.
[2025-04-28 21:21:21,567 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:21,567 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,568 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,568 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:21,568 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,571 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,571 INFO  L85        PathProgramCache]: Analyzing trace with hash 1238194142, now seen corresponding path program 1 times
[2025-04-28 21:21:21,571 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,571 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [719917059]
[2025-04-28 21:21:21,572 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,572 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,584 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:21,601 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:21,601 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,601 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,072 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:22,072 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,073 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [719917059]
[2025-04-28 21:21:22,073 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [719917059] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,073 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1119980343]
[2025-04-28 21:21:22,073 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,073 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,080 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,087 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:22,088 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,146 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:22,180 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:22,181 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,181 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,183 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 29 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,193 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:22,489 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:22,489 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:23,654 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:23,655 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1119980343] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:23,655 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:23,655 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 21
[2025-04-28 21:21:23,658 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [876568821]
[2025-04-28 21:21:23,658 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,659 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:23,659 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,660 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:23,660 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=60, Invalid=360, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:23,661 INFO  L87              Difference]: Start difference. First operand 41 states and 51 transitions. Second operand  has 21 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 21 states have internal predecessors, (25), 11 states have call successors, (13), 1 states have call predecessors, (13), 12 states have return successors, (18), 11 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:23,915 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,915 INFO  L93              Difference]: Finished difference Result 53 states and 67 transitions.
[2025-04-28 21:21:23,916 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:23,917 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 21 states have internal predecessors, (25), 11 states have call successors, (13), 1 states have call predecessors, (13), 12 states have return successors, (18), 11 states have call predecessors, (18), 11 states have call successors, (18) Word has length 32
[2025-04-28 21:21:23,917 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,918 INFO  L225             Difference]: With dead ends: 53
[2025-04-28 21:21:23,918 INFO  L226             Difference]: Without dead ends: 51
[2025-04-28 21:21:23,919 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 76 GetRequests, 56 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 54 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=66, Invalid=396, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:23,920 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 8 mSDsluCounter, 282 mSDsCounter, 0 mSdLazyCounter, 127 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 317 SdHoareTripleChecker+Invalid, 133 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 127 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,920 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 317 Invalid, 133 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 127 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:23,925 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 51 states.
[2025-04-28 21:21:23,937 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 51 to 43.
[2025-04-28 21:21:23,938 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 43 states, 19 states have (on average 1.2105263157894737) internal successors, (23), 23 states have internal predecessors, (23), 11 states have call successors, (11), 7 states have call predecessors, (11), 12 states have return successors, (20), 12 states have call predecessors, (20), 11 states have call successors, (20)
[2025-04-28 21:21:23,939 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 43 states to 43 states and 54 transitions.
[2025-04-28 21:21:23,939 INFO  L79                 Accepts]: Start accepts. Automaton has 43 states and 54 transitions. Word has length 32
[2025-04-28 21:21:23,941 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,942 INFO  L485      AbstractCegarLoop]: Abstraction has 43 states and 54 transitions.
[2025-04-28 21:21:23,942 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 21 states have internal predecessors, (25), 11 states have call successors, (13), 1 states have call predecessors, (13), 12 states have return successors, (18), 11 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:23,942 INFO  L278                IsEmpty]: Start isEmpty. Operand 43 states and 54 transitions.
[2025-04-28 21:21:23,944 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:23,944 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,944 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,951 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:24,149 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,150 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,150 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,151 INFO  L85        PathProgramCache]: Analyzing trace with hash -873087949, now seen corresponding path program 1 times
[2025-04-28 21:21:24,151 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,151 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1694856947]
[2025-04-28 21:21:24,151 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,151 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,159 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:24,170 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:24,170 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,170 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:24,170 INFO  L348             TraceCheck]: Trace is feasible, we will do another trace check, this time with branch encoders.
[2025-04-28 21:21:24,174 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:24,184 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:24,184 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,184 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is sat
[2025-04-28 21:21:24,199 INFO  L130   FreeRefinementEngine]: Strategy CAMEL found a feasible trace
[2025-04-28 21:21:24,200 INFO  L340         BasicCegarLoop]: Counterexample is feasible
[2025-04-28 21:21:24,201 INFO  L790   garLoopResultBuilder]: Registering result UNSAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:24,203 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:24,206 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1]
[2025-04-28 21:21:24,220 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:24,223 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:24 BoogieIcfgContainer
[2025-04-28 21:21:24,224 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:24,225 INFO  L158              Benchmark]: Toolchain (without parser) took 4354.56ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 163.4MB in the beginning and 116.1MB in the end (delta: 47.3MB). Peak memory consumption was 1.1MB. Max. memory is 33.6GB.
[2025-04-28 21:21:24,225 INFO  L158              Benchmark]: SmtParser took 0.47ms. Allocated memory is still 234.9MB. Free memory is still 171.4MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:24,225 INFO  L158              Benchmark]: ChcToBoogie took 33.05ms. Allocated memory is still 234.9MB. Free memory was 163.4MB in the beginning and 162.7MB in the end (delta: 727.1kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:24,226 INFO  L158              Benchmark]: Boogie Preprocessor took 87.75ms. Allocated memory is still 234.9MB. Free memory was 162.7MB in the beginning and 160.5MB in the end (delta: 2.2MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:24,226 INFO  L158              Benchmark]: RCFGBuilder took 334.30ms. Allocated memory is still 234.9MB. Free memory was 160.5MB in the beginning and 150.3MB in the end (delta: 10.2MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:24,226 INFO  L158              Benchmark]: TraceAbstraction took 3893.06ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 150.3MB in the beginning and 116.1MB in the end (delta: 34.1MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:24,228 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.47ms. Allocated memory is still 234.9MB. Free memory is still 171.4MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 33.05ms. Allocated memory is still 234.9MB. Free memory was 163.4MB in the beginning and 162.7MB in the end (delta: 727.1kB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 87.75ms. Allocated memory is still 234.9MB. Free memory was 162.7MB in the beginning and 160.5MB in the end (delta: 2.2MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 334.30ms. Allocated memory is still 234.9MB. Free memory was 160.5MB in the beginning and 150.3MB in the end (delta: 10.2MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 3893.06ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 150.3MB in the beginning and 116.1MB in the end (delta: 34.1MB). There was no memory consumed. 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]        assume hbv_False_B_1 != hbv_False_A_2;
      VAL   [hbv_False_A_2=1, hbv_False_B_1=5]
[L0]  CALL  call inv_main37(hbv_False_C_3, hbv_False_B_1, hbv_False_A_2);
      VAL   [hhv_inv_main37_A_2=1, hhv_inv_main37_D_1=5, hhv_inv_main37_F_0=1]
[L0]        assume !(hbv_inv_main37_C_3 != 0 && hbv_inv_main37_E_1 <= hbv_inv_main37_B_2);
      VAL   [hbv_inv_main37_B_2=1, hbv_inv_main37_E_1=1, hhv_inv_main37_A_2=1, hhv_inv_main37_D_1=5, hhv_inv_main37_F_0=1]
[L0]  CALL  call inv_main31(hhv_inv_main37_F_0, hhv_inv_main37_D_1, hbv_inv_main37_B_2, hbv_inv_main37_E_1, hhv_inv_main37_A_2);
      VAL   [hhv_inv_main31_A_4=1, hhv_inv_main31_C_2=1, hhv_inv_main31_D_1=5, hhv_inv_main31_F_0=1, hhv_inv_main31_v_6_3=1]
[L0]        assume hhv_inv_main31_v_6_3 == 1 && !(hbv_inv_main31_E_1 <= hhv_inv_main31_C_2 && hbv_inv_main31_B_2 != 0);
      VAL   [hbv_inv_main31_E_1=1, hhv_inv_main31_A_4=1, hhv_inv_main31_C_2=1, hhv_inv_main31_D_1=5, hhv_inv_main31_F_0=1, hhv_inv_main31_v_6_3=1]
[L0]  CALL  call inv_main25(hhv_inv_main31_F_0, hhv_inv_main31_D_1, hhv_inv_main31_C_2, hbv_inv_main31_E_1, hhv_inv_main31_A_4);
      VAL   [hhv_inv_main25_A_4=1, hhv_inv_main25_B_3=1, hhv_inv_main25_E_2=1, hhv_inv_main25_F_1=5, hhv_inv_main25_H_0=1]
[L0]        assume ((!(hbv_inv_main25_D_3 != 0 && hbv_inv_main25_G_1 <= hbv_inv_main25_C_2) && hhv_inv_main25_E_2 == hhv_inv_main25_H_0) && hhv_inv_main25_A_4 == 1) && hhv_inv_main25_B_3 == 1;
      VAL   [hbv_inv_main25_C_2=1, hbv_inv_main25_G_1=0, hhv_inv_main25_A_4=1, hhv_inv_main25_B_3=1, hhv_inv_main25_E_2=1, hhv_inv_main25_F_1=5, hhv_inv_main25_H_0=1]
[L0]  CALL  call inv_main14(hhv_inv_main25_H_0, hbv_inv_main25_C_2, hbv_inv_main25_G_1, hhv_inv_main25_F_1);
      VAL   [hhv_inv_main14_C_1=1, hhv_inv_main14_D_3=5, hhv_inv_main14_E_0=1, hhv_inv_main14_v_5_2=0]
[L0]        assume hhv_inv_main14_v_5_2 == 0 && !(hbv_inv_main14_B_2 != 0 && hbv_inv_main14_A_1 <= hhv_inv_main14_C_1);
      VAL   [hbv_inv_main14_A_1=2, hhv_inv_main14_C_1=1, hhv_inv_main14_D_3=5, hhv_inv_main14_E_0=1, hhv_inv_main14_v_5_2=0]
[L0]  CALL  call inv_main8(hhv_inv_main14_E_0, hhv_inv_main14_C_1, hbv_inv_main14_A_1, hhv_inv_main14_D_3);
      VAL   [hhv_inv_main8_A_3=5, hhv_inv_main8_B_2=2, hhv_inv_main8_E_1=1, hhv_inv_main8_G_0=1]
[L0]        assume ((hbv_inv_main8_C_3 != 0 && hhv_inv_main8_B_2 == hbv_inv_main8_D_1 + 1) && hhv_inv_main8_A_3 == 5 * hbv_inv_main8_F_2) && !(hhv_inv_main8_E_1 < hbv_inv_main8_D_1);
      VAL   [hbv_inv_main8_D_1=1, hbv_inv_main8_F_2=1, hhv_inv_main8_A_3=5, hhv_inv_main8_B_2=2, hhv_inv_main8_E_1=1, hhv_inv_main8_G_0=1]
[L0]  CALL  call inv_main8(hhv_inv_main8_G_0, hhv_inv_main8_E_1, hbv_inv_main8_D_1, hbv_inv_main8_F_2);
      VAL   [hhv_inv_main8_A_3=1, hhv_inv_main8_B_2=1, hhv_inv_main8_E_1=1, hhv_inv_main8_G_0=1]
[L0]        assume (hhv_inv_main8_A_3 == 1 && hhv_inv_main8_E_1 == hhv_inv_main8_G_0) && hhv_inv_main8_B_2 == 1;
      VAL   [hhv_inv_main8_A_3=1, hhv_inv_main8_B_2=1, hhv_inv_main8_E_1=1, hhv_inv_main8_G_0=1]
[L0]  CALL  call inv_main3(hhv_inv_main8_G_0);
[L0]  RET   call inv_main3(hhv_inv_main8_G_0);
      VAL   [hhv_inv_main8_A_3=1, hhv_inv_main8_B_2=1, hhv_inv_main8_E_1=1, hhv_inv_main8_G_0=1]
[L0]  RET   call inv_main8(hhv_inv_main8_G_0, hhv_inv_main8_E_1, hbv_inv_main8_D_1, hbv_inv_main8_F_2);
      VAL   [hbv_inv_main8_D_1=1, hbv_inv_main8_F_2=1, hhv_inv_main8_A_3=5, hhv_inv_main8_B_2=2, hhv_inv_main8_E_1=1, hhv_inv_main8_G_0=1]
[L0]  RET   call inv_main8(hhv_inv_main14_E_0, hhv_inv_main14_C_1, hbv_inv_main14_A_1, hhv_inv_main14_D_3);
      VAL   [hbv_inv_main14_A_1=2, hhv_inv_main14_C_1=1, hhv_inv_main14_D_3=5, hhv_inv_main14_E_0=1, hhv_inv_main14_v_5_2=0]
[L0]  RET   call inv_main14(hhv_inv_main25_H_0, hbv_inv_main25_C_2, hbv_inv_main25_G_1, hhv_inv_main25_F_1);
      VAL   [hbv_inv_main25_C_2=1, hbv_inv_main25_G_1=0, hhv_inv_main25_A_4=1, hhv_inv_main25_B_3=1, hhv_inv_main25_E_2=1, hhv_inv_main25_F_1=5, hhv_inv_main25_H_0=1]
[L0]  RET   call inv_main25(hhv_inv_main31_F_0, hhv_inv_main31_D_1, hhv_inv_main31_C_2, hbv_inv_main31_E_1, hhv_inv_main31_A_4);
      VAL   [hbv_inv_main31_E_1=1, hhv_inv_main31_A_4=1, hhv_inv_main31_C_2=1, hhv_inv_main31_D_1=5, hhv_inv_main31_F_0=1, hhv_inv_main31_v_6_3=1]
[L0]  RET   call inv_main31(hhv_inv_main37_F_0, hhv_inv_main37_D_1, hbv_inv_main37_B_2, hbv_inv_main37_E_1, hhv_inv_main37_A_2);
      VAL   [hbv_inv_main37_B_2=1, hbv_inv_main37_E_1=1, hhv_inv_main37_A_2=1, hhv_inv_main37_D_1=5, hhv_inv_main37_F_0=1]
[L0]  RET   call inv_main37(hbv_False_C_3, hbv_False_B_1, hbv_False_A_2);
      VAL   [hbv_False_A_2=1, hbv_False_B_1=5, hbv_False_C_3=1]
[L0]  RET   call False();
[L0]        assert false;

  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 8 procedures, 35 locations, 53 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 3.8s, OverallIterations: 3, TraceHistogramMax: 2, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.6s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 22 SdHoareTripleChecker+Valid, 0.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 11 mSDsluCounter, 552 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 485 mSDsCounter, 6 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 205 IncrementalHoareTripleChecker+Invalid, 211 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 6 mSolverCounterUnsat, 67 mSDtfsCounter, 205 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 86 GetRequests, 58 SyntacticMatches, 0 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 54 ImplicationChecksByTransitivity, 0.6s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=43occurred in iteration=2, InterpolantAutomatonStates: 21, 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, 10 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 2.5s InterpolantComputationTime, 124 NumberOfCodeBlocks, 124 NumberOfCodeBlocksAsserted, 4 NumberOfCheckSat, 120 ConstructedInterpolants, 0 QuantifiedInterpolants, 355 SizeOfPredicates, 2 NumberOfNonLiveVariables, 115 ConjunctsInSsa, 29 ConjunctsInUnsatCore, 4 InterpolantComputations, 1 PerfectInterpolantSequences, 3/9 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:24,243 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
