./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-133.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:13,604 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:13,699 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bbee74f9-73b2-4029-b439-97609abe2dbb/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:13,704 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:13,705 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:13,734 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:13,735 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:13,735 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:13,735 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:13,736 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:13,736 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:13,736 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:13,736 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:13,736 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:13,738 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:13,739 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:13,739 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:13,739 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:13,739 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,740 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:13,740 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:13,740 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:13,740 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:13,740 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:13,741 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:13,741 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:13,741 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:14,130 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:14,142 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:14,145 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:14,148 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:14,149 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:14,151 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bbee74f9-73b2-4029-b439-97609abe2dbb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-133.smt2
[2025-04-28 21:21:14,154 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:14,158 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:14,431 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bbee74f9-73b2-4029-b439-97609abe2dbb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-133.smt2
[2025-04-28 21:21:14,436 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:14,439 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:14,440 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:14,442 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:14,443 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:14,446 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,484 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14 Unit
[2025-04-28 21:21:14,484 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:14,486 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,487 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:14,487 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:14,507 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,507 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,546 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,547 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,551 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,553 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,559 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,560 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,560 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,576 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,577 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:14,577 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:14,577 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:14,578 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,581 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,597 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,617 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:14,622 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:14,639 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:14,640 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:14,640 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:14,640 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:14,640 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:14,640 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:14,641 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lock.DLRunknown.CLN7 given in one single declaration
[2025-04-28 21:21:14,641 INFO  L130     BoogieDeclarations]: Found specification of procedure lock.DLRunknown.CLN7
[2025-04-28 21:21:14,641 INFO  L138     BoogieDeclarations]: Found implementation of procedure lock.DLRunknown.CLN7
[2025-04-28 21:21:14,641 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure f.DLRunknown.CLN2 given in one single declaration
[2025-04-28 21:21:14,641 INFO  L130     BoogieDeclarations]: Found specification of procedure f.DLRunknown.CLN2
[2025-04-28 21:21:14,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure f.DLRunknown.CLN2
[2025-04-28 21:21:14,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure unlock.DLRunknown.CLN9 given in one single declaration
[2025-04-28 21:21:14,642 INFO  L130     BoogieDeclarations]: Found specification of procedure unlock.DLRunknown.CLN9
[2025-04-28 21:21:14,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure unlock.DLRunknown.CLN9
[2025-04-28 21:21:14,642 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure g.DLRunknown.CLN5 given in one single declaration
[2025-04-28 21:21:14,642 INFO  L130     BoogieDeclarations]: Found specification of procedure g.DLRunknown.CLN5
[2025-04-28 21:21:14,642 INFO  L138     BoogieDeclarations]: Found implementation of procedure g.DLRunknown.CLN5
[2025-04-28 21:21:14,643 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure g.DLRunknown.CLN6 given in one single declaration
[2025-04-28 21:21:14,643 INFO  L130     BoogieDeclarations]: Found specification of procedure g.DLRunknown.CLN6
[2025-04-28 21:21:14,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure g.DLRunknown.CLN6
[2025-04-28 21:21:14,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure unlock.DLRunknown.CLN10 given in one single declaration
[2025-04-28 21:21:14,644 INFO  L130     BoogieDeclarations]: Found specification of procedure unlock.DLRunknown.CLN10
[2025-04-28 21:21:14,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure unlock.DLRunknown.CLN10
[2025-04-28 21:21:14,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure f.DLRunknown.CLN3 given in one single declaration
[2025-04-28 21:21:14,644 INFO  L130     BoogieDeclarations]: Found specification of procedure f.DLRunknown.CLN3
[2025-04-28 21:21:14,644 INFO  L138     BoogieDeclarations]: Found implementation of procedure f.DLRunknown.CLN3
[2025-04-28 21:21:14,644 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lock.DLRunknown.CLN8 given in one single declaration
[2025-04-28 21:21:14,644 INFO  L130     BoogieDeclarations]: Found specification of procedure lock.DLRunknown.CLN8
[2025-04-28 21:21:14,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure lock.DLRunknown.CLN8
[2025-04-28 21:21:14,645 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:14,645 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:14,645 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:14,713 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:14,716 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:14,964 INFO  L?                        ?]: Removed 16 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:14,964 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:14,987 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:14,989 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:14,990 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14 BoogieIcfgContainer
[2025-04-28 21:21:14,990 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:14,994 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:14,994 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:15,000 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:15,001 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/3) ...
[2025-04-28 21:21:15,003 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@44520c81 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:15, skipping insertion in model container
[2025-04-28 21:21:15,003 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (2/3) ...
[2025-04-28 21:21:15,003 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@44520c81 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:15, skipping insertion in model container
[2025-04-28 21:21:15,003 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14" (3/3) ...
[2025-04-28 21:21:15,005 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:15,027 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:15,031 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 11 procedures, 50 locations, 77 edges, 11 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:15,091 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:15,108 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;@37eb3b9a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:15,110 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:15,120 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 50 states, 21 states have (on average 1.2380952380952381) internal successors, (26), 26 states have internal predecessors, (26), 17 states have call successors, (17), 10 states have call predecessors, (17), 10 states have return successors, (17), 13 states have call predecessors, (17), 17 states have call successors, (17)
[2025-04-28 21:21:15,135 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:15,136 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,136 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,137 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,142 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,142 INFO  L85        PathProgramCache]: Analyzing trace with hash -404858090, now seen corresponding path program 1 times
[2025-04-28 21:21:15,149 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,149 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2110748518]
[2025-04-28 21:21:15,150 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,151 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,181 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:15,202 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:15,203 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,203 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,414 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:15,415 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,415 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2110748518]
[2025-04-28 21:21:15,419 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2110748518] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,420 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,423 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:15,425 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [738539817]
[2025-04-28 21:21:15,426 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:15,432 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:15,432 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:15,462 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:15,463 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:15,467 INFO  L87              Difference]: Start difference. First operand  has 50 states, 21 states have (on average 1.2380952380952381) internal successors, (26), 26 states have internal predecessors, (26), 17 states have call successors, (17), 10 states have call predecessors, (17), 10 states have return successors, (17), 13 states have call predecessors, (17), 17 states have call successors, (17) Second operand  has 5 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:15,605 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:15,606 INFO  L93              Difference]: Finished difference Result 50 states and 59 transitions.
[2025-04-28 21:21:15,607 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:15,609 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:15,609 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:15,619 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:15,620 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:15,624 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:15,630 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 1 mSDsluCounter, 151 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 206 SdHoareTripleChecker+Invalid, 22 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:15,631 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 206 Invalid, 22 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:15,682 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:15,748 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 47.
[2025-04-28 21:21:15,750 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 20 states have (on average 1.15) internal successors, (23), 23 states have internal predecessors, (23), 16 states have call successors, (16), 10 states have call predecessors, (16), 10 states have return successors, (16), 13 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:15,754 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 55 transitions.
[2025-04-28 21:21:15,757 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 55 transitions. Word has length 16
[2025-04-28 21:21:15,757 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:15,757 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 55 transitions.
[2025-04-28 21:21:15,758 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.0) internal successors, (8), 5 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:15,758 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 55 transitions.
[2025-04-28 21:21:15,760 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:15,761 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,762 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]
[2025-04-28 21:21:15,762 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:15,762 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,764 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,764 INFO  L85        PathProgramCache]: Analyzing trace with hash 594740952, now seen corresponding path program 1 times
[2025-04-28 21:21:15,764 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,764 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1694603582]
[2025-04-28 21:21:15,765 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,765 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,780 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:15,799 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:15,803 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,803 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,994 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:15,994 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,994 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1694603582]
[2025-04-28 21:21:15,994 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1694603582] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:15,998 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:15,999 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:15,999 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1332376343]
[2025-04-28 21:21:15,999 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,000 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:16,000 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,001 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:16,001 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:16,002 INFO  L87              Difference]: Start difference. First operand 47 states and 55 transitions. Second operand  has 5 states, 4 states have (on average 3.0) internal successors, (12), 5 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:16,104 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,105 INFO  L93              Difference]: Finished difference Result 51 states and 61 transitions.
[2025-04-28 21:21:16,106 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:16,106 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 3.0) internal successors, (12), 5 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:16,106 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,107 INFO  L225             Difference]: With dead ends: 51
[2025-04-28 21:21:16,111 INFO  L226             Difference]: Without dead ends: 51
[2025-04-28 21:21:16,112 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:16,113 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 1 mSDsluCounter, 153 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 208 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 21 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,114 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 208 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 21 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:16,115 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 51 states.
[2025-04-28 21:21:16,146 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 51 to 51.
[2025-04-28 21:21:16,147 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 22 states have (on average 1.1363636363636365) internal successors, (25), 25 states have internal predecessors, (25), 16 states have call successors, (16), 10 states have call predecessors, (16), 12 states have return successors, (20), 15 states have call predecessors, (20), 16 states have call successors, (20)
[2025-04-28 21:21:16,153 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 61 transitions.
[2025-04-28 21:21:16,154 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 61 transitions. Word has length 24
[2025-04-28 21:21:16,154 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,154 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 61 transitions.
[2025-04-28 21:21:16,154 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 3.0) internal successors, (12), 5 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:16,155 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 61 transitions.
[2025-04-28 21:21:16,156 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:16,156 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,156 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 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:16,161 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:16,162 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,163 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,163 INFO  L85        PathProgramCache]: Analyzing trace with hash 1825448668, now seen corresponding path program 1 times
[2025-04-28 21:21:16,163 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,163 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1239800149]
[2025-04-28 21:21:16,163 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,163 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,194 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:16,213 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:16,216 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,216 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,656 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:16,656 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,656 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1239800149]
[2025-04-28 21:21:16,656 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1239800149] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:16,656 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [631867558]
[2025-04-28 21:21:16,656 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,657 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:16,660 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,664 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:16,667 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:16,729 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:16,759 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:16,759 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,759 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,762 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:16,768 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:16,927 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 0 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:16,927 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:17,266 INFO  L134       CoverageAnalysis]: Checked inductivity of 7 backedges. 0 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:17,267 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [631867558] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:17,267 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:17,267 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 6, 6] total 13
[2025-04-28 21:21:17,267 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1924111482]
[2025-04-28 21:21:17,267 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,268 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:17,268 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,272 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:17,272 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:17,272 INFO  L87              Difference]: Start difference. First operand 51 states and 61 transitions. Second operand  has 13 states, 6 states have (on average 3.3333333333333335) internal successors, (20), 10 states have internal predecessors, (20), 10 states have call successors, (13), 1 states have call predecessors, (13), 6 states have return successors, (13), 8 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:17,434 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,435 INFO  L93              Difference]: Finished difference Result 58 states and 69 transitions.
[2025-04-28 21:21:17,435 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:17,436 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 3.3333333333333335) internal successors, (20), 10 states have internal predecessors, (20), 10 states have call successors, (13), 1 states have call predecessors, (13), 6 states have return successors, (13), 8 states have call predecessors, (13), 10 states have call successors, (13) Word has length 32
[2025-04-28 21:21:17,436 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,437 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:21:17,437 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:21:17,438 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 72 GetRequests, 60 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 25 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=41, Invalid=141, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:17,439 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 4 mSDsluCounter, 354 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 409 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,439 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 409 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,440 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:21:17,448 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 54.
[2025-04-28 21:21:17,448 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 54 states, 23 states have (on average 1.1304347826086956) internal successors, (26), 26 states have internal predecessors, (26), 17 states have call successors, (17), 10 states have call predecessors, (17), 13 states have return successors, (22), 17 states have call predecessors, (22), 17 states have call successors, (22)
[2025-04-28 21:21:17,450 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 65 transitions.
[2025-04-28 21:21:17,451 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 65 transitions. Word has length 32
[2025-04-28 21:21:17,451 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,452 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 65 transitions.
[2025-04-28 21:21:17,452 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 3.3333333333333335) internal successors, (20), 10 states have internal predecessors, (20), 10 states have call successors, (13), 1 states have call predecessors, (13), 6 states have return successors, (13), 8 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:17,452 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 65 transitions.
[2025-04-28 21:21:17,454 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:17,455 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,455 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 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, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,461 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:17,659 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:17,660 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,660 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,661 INFO  L85        PathProgramCache]: Analyzing trace with hash -1046911621, now seen corresponding path program 1 times
[2025-04-28 21:21:17,661 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,661 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [98224722]
[2025-04-28 21:21:17,661 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,661 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,669 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:17,685 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:17,685 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,685 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,930 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:17,930 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,930 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [98224722]
[2025-04-28 21:21:17,930 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [98224722] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:17,930 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1708174989]
[2025-04-28 21:21:17,931 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,931 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:17,935 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:17,937 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:17,941 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:17,989 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:18,017 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:18,017 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,017 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,019 INFO  L256         TraceCheckSpWp]: Trace formula consists of 126 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,022 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:18,287 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:18,287 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:19,396 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:19,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1708174989] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:19,397 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:19,397 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 20
[2025-04-28 21:21:19,397 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [787925238]
[2025-04-28 21:21:19,397 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,398 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:19,398 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,399 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:19,399 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=330, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:19,400 INFO  L87              Difference]: Start difference. First operand 54 states and 65 transitions. Second operand  has 20 states, 13 states have (on average 2.3076923076923075) internal successors, (30), 18 states have internal predecessors, (30), 13 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (23), 18 states have call predecessors, (23), 13 states have call successors, (23)
[2025-04-28 21:21:19,607 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,608 INFO  L93              Difference]: Finished difference Result 61 states and 72 transitions.
[2025-04-28 21:21:19,608 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:19,608 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 13 states have (on average 2.3076923076923075) internal successors, (30), 18 states have internal predecessors, (30), 13 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (23), 18 states have call predecessors, (23), 13 states have call successors, (23) Word has length 44
[2025-04-28 21:21:19,609 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,610 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:19,610 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:19,610 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 100 GetRequests, 74 SyntacticMatches, 5 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 74 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=68, Invalid=438, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:19,611 INFO  L437           NwaCegarLoop]: 60 mSDtfsCounter, 5 mSDsluCounter, 606 mSDsCounter, 0 mSdLazyCounter, 122 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 666 SdHoareTripleChecker+Invalid, 127 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 122 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,611 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 666 Invalid, 127 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 122 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,612 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:19,619 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:19,619 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 24 states have (on average 1.125) internal successors, (27), 27 states have internal predecessors, (27), 18 states have call successors, (18), 10 states have call predecessors, (18), 14 states have return successors, (23), 19 states have call predecessors, (23), 18 states have call successors, (23)
[2025-04-28 21:21:19,620 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 68 transitions.
[2025-04-28 21:21:19,621 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 68 transitions. Word has length 44
[2025-04-28 21:21:19,621 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,621 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 68 transitions.
[2025-04-28 21:21:19,621 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 13 states have (on average 2.3076923076923075) internal successors, (30), 18 states have internal predecessors, (30), 13 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (23), 18 states have call predecessors, (23), 13 states have call successors, (23)
[2025-04-28 21:21:19,622 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 68 transitions.
[2025-04-28 21:21:19,623 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:19,623 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,623 INFO  L218           NwaCegarLoop]: trace histogram [2, 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, 1, 1]
[2025-04-28 21:21:19,628 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:19,827 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:19,828 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,828 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,828 INFO  L85        PathProgramCache]: Analyzing trace with hash 755115639, now seen corresponding path program 1 times
[2025-04-28 21:21:19,828 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,828 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1949973185]
[2025-04-28 21:21:19,828 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,828 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,834 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:19,847 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:19,848 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,848 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,005 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:20,005 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,006 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1949973185]
[2025-04-28 21:21:20,006 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1949973185] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,006 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,006 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:20,006 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [144000543]
[2025-04-28 21:21:20,006 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,007 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:20,007 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,007 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:20,007 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:20,008 INFO  L87              Difference]: Start difference. First operand 57 states and 68 transitions. Second operand  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 4 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 7 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:20,116 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,116 INFO  L93              Difference]: Finished difference Result 57 states and 67 transitions.
[2025-04-28 21:21:20,116 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:20,117 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 4 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 7 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:21:20,117 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,118 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:21:20,118 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:20,118 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:20,119 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 1 mSDsluCounter, 271 mSDsCounter, 0 mSdLazyCounter, 60 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 320 SdHoareTripleChecker+Invalid, 60 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 60 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,119 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 320 Invalid, 60 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 60 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:20,120 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:20,125 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:20,126 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 24 states have (on average 1.0833333333333333) internal successors, (26), 26 states have internal predecessors, (26), 17 states have call successors, (17), 10 states have call predecessors, (17), 14 states have return successors, (22), 19 states have call predecessors, (22), 17 states have call successors, (22)
[2025-04-28 21:21:20,127 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 65 transitions.
[2025-04-28 21:21:20,127 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 65 transitions. Word has length 36
[2025-04-28 21:21:20,127 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,127 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 65 transitions.
[2025-04-28 21:21:20,128 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 4 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 7 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:20,128 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 65 transitions.
[2025-04-28 21:21:20,129 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 57
[2025-04-28 21:21:20,129 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,130 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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,130 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:20,130 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,130 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,131 INFO  L85        PathProgramCache]: Analyzing trace with hash -1411738086, now seen corresponding path program 1 times
[2025-04-28 21:21:20,131 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,131 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [465277480]
[2025-04-28 21:21:20,131 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,131 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,140 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 56 statements into 1 equivalence classes.
[2025-04-28 21:21:20,151 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 56 of 56 statements.
[2025-04-28 21:21:20,151 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,151 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,324 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:20,325 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,325 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [465277480]
[2025-04-28 21:21:20,325 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [465277480] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:20,325 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [76472156]
[2025-04-28 21:21:20,325 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,325 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,328 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,330 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:20,336 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:20,379 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 56 statements into 1 equivalence classes.
[2025-04-28 21:21:20,404 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 56 of 56 statements.
[2025-04-28 21:21:20,405 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,405 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,406 INFO  L256         TraceCheckSpWp]: Trace formula consists of 158 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:20,408 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:20,442 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:20,443 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:20,904 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:20,904 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [76472156] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:20,904 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:20,904 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 5
[2025-04-28 21:21:20,904 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1838169772]
[2025-04-28 21:21:20,904 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,905 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:20,905 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,908 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:20,909 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:20,909 INFO  L87              Difference]: Start difference. First operand 56 states and 65 transitions. Second operand  has 5 states, 4 states have (on average 4.5) internal successors, (18), 4 states have internal predecessors, (18), 4 states have call successors, (12), 1 states have call predecessors, (12), 4 states have return successors, (12), 5 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:20,942 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,942 INFO  L93              Difference]: Finished difference Result 58 states and 66 transitions.
[2025-04-28 21:21:20,944 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:20,944 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 4 states have internal predecessors, (18), 4 states have call successors, (12), 1 states have call predecessors, (12), 4 states have return successors, (12), 5 states have call predecessors, (12), 4 states have call successors, (12) Word has length 56
[2025-04-28 21:21:20,945 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,945 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:21:20,945 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:20,946 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 116 GetRequests, 110 SyntacticMatches, 3 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:20,946 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 1 mSDsluCounter, 147 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 200 SdHoareTripleChecker+Invalid, 13 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,947 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 200 Invalid, 13 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:20,948 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:20,954 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 53.
[2025-04-28 21:21:20,955 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 53 states, 23 states have (on average 1.0434782608695652) internal successors, (24), 24 states have internal predecessors, (24), 16 states have call successors, (16), 10 states have call predecessors, (16), 13 states have return successors, (20), 18 states have call predecessors, (20), 16 states have call successors, (20)
[2025-04-28 21:21:20,956 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 60 transitions.
[2025-04-28 21:21:20,956 INFO  L79                 Accepts]: Start accepts. Automaton has 53 states and 60 transitions. Word has length 56
[2025-04-28 21:21:20,961 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,961 INFO  L485      AbstractCegarLoop]: Abstraction has 53 states and 60 transitions.
[2025-04-28 21:21:20,961 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 4.5) internal successors, (18), 4 states have internal predecessors, (18), 4 states have call successors, (12), 1 states have call predecessors, (12), 4 states have return successors, (12), 5 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:20,962 INFO  L278                IsEmpty]: Start isEmpty. Operand 53 states and 60 transitions.
[2025-04-28 21:21:20,963 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 89
[2025-04-28 21:21:20,963 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,964 INFO  L218           NwaCegarLoop]: trace histogram [6, 6, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 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]
[2025-04-28 21:21:20,974 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:21,168 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,168 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,168 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,168 INFO  L85        PathProgramCache]: Analyzing trace with hash 1794765222, now seen corresponding path program 1 times
[2025-04-28 21:21:21,169 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,169 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1447908675]
[2025-04-28 21:21:21,169 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,169 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,181 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 88 statements into 1 equivalence classes.
[2025-04-28 21:21:21,201 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 88 of 88 statements.
[2025-04-28 21:21:21,202 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,202 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,351 INFO  L134       CoverageAnalysis]: Checked inductivity of 88 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 88 trivial. 0 not checked.
[2025-04-28 21:21:21,351 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,351 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1447908675]
[2025-04-28 21:21:21,351 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1447908675] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,352 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,352 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:21,352 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [379586962]
[2025-04-28 21:21:21,352 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,352 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:21,352 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,353 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:21,353 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:21,353 INFO  L87              Difference]: Start difference. First operand 53 states and 60 transitions. Second operand  has 6 states, 4 states have (on average 5.0) internal successors, (20), 6 states have internal predecessors, (20), 4 states have call successors, (13), 1 states have call predecessors, (13), 4 states have return successors, (13), 6 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:21:21,384 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,384 INFO  L93              Difference]: Finished difference Result 47 states and 52 transitions.
[2025-04-28 21:21:21,384 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:21,385 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 5.0) internal successors, (20), 6 states have internal predecessors, (20), 4 states have call successors, (13), 1 states have call predecessors, (13), 4 states have return successors, (13), 6 states have call predecessors, (13), 4 states have call successors, (13) Word has length 88
[2025-04-28 21:21:21,385 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,385 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:21,385 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:21,386 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,386 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 1 mSDsluCounter, 154 mSDsCounter, 0 mSdLazyCounter, 8 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 196 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 8 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,387 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 196 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 8 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:21,388 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:21,388 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:21,388 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:21,388 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:21,388 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 88
[2025-04-28 21:21:21,388 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,388 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:21,388 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 5.0) internal successors, (20), 6 states have internal predecessors, (20), 4 states have call successors, (13), 1 states have call predecessors, (13), 4 states have return successors, (13), 6 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:21:21,389 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:21,389 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:21,391 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:21,392 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:21,395 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,397 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:21,414 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:21 BoogieIcfgContainer
[2025-04-28 21:21:21,415 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:21,416 INFO  L158              Benchmark]: Toolchain (without parser) took 6976.53ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 162.9MB in the beginning and 142.9MB in the end (delta: 20.1MB). Peak memory consumption was 58.7MB. Max. memory is 33.6GB.
[2025-04-28 21:21:21,416 INFO  L158              Benchmark]: SmtParser took 1.41ms. Allocated memory is still 234.9MB. Free memory is still 171.1MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:21,416 INFO  L158              Benchmark]: ChcToBoogie took 45.48ms. Allocated memory is still 234.9MB. Free memory was 162.9MB in the beginning and 161.9MB in the end (delta: 1.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:21,416 INFO  L158              Benchmark]: Boogie Preprocessor took 89.85ms. Allocated memory is still 234.9MB. Free memory was 161.9MB in the beginning and 159.5MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:21,417 INFO  L158              Benchmark]: RCFGBuilder took 413.94ms. Allocated memory is still 234.9MB. Free memory was 159.5MB in the beginning and 148.6MB in the end (delta: 10.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:21,418 INFO  L158              Benchmark]: TraceAbstraction took 6420.48ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 148.3MB in the beginning and 142.9MB in the end (delta: 5.4MB). Peak memory consumption was 41.9MB. Max. memory is 33.6GB.
[2025-04-28 21:21:21,419 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.41ms. Allocated memory is still 234.9MB. Free memory is still 171.1MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 45.48ms. Allocated memory is still 234.9MB. Free memory was 162.9MB in the beginning and 161.9MB in the end (delta: 1.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 89.85ms. Allocated memory is still 234.9MB. Free memory was 161.9MB in the beginning and 159.5MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 413.94ms. Allocated memory is still 234.9MB. Free memory was 159.5MB in the beginning and 148.6MB in the end (delta: 10.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 6420.48ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 148.3MB in the beginning and 142.9MB in the end (delta: 5.4MB). Peak memory consumption was 41.9MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 11 procedures, 50 locations, 77 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 6.3s, OverallIterations: 7, TraceHistogramMax: 6, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.9s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 29 SdHoareTripleChecker+Valid, 0.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 14 mSDsluCounter, 2205 SdHoareTripleChecker+Invalid, 0.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 1836 mSDsCounter, 11 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 303 IncrementalHoareTripleChecker+Invalid, 314 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 11 mSolverCounterUnsat, 369 mSDtfsCounter, 303 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 314 GetRequests, 252 SyntacticMatches, 8 SemanticMatches, 54 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 99 ImplicationChecksByTransitivity, 0.8s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=57occurred in iteration=4, InterpolantAutomatonStates: 47, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.2s AutomataMinimizationTime, 7 MinimizatonAttempts, 10 StatesRemovedByMinimization, 4 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.2s SatisfiabilityAnalysisTime, 3.9s InterpolantComputationTime, 428 NumberOfCodeBlocks, 428 NumberOfCodeBlocksAsserted, 10 NumberOfCheckSat, 547 ConstructedInterpolants, 0 QuantifiedInterpolants, 901 SizeOfPredicates, 6 NumberOfNonLiveVariables, 378 ConjunctsInSsa, 34 ConjunctsInUnsatCore, 13 InterpolantComputations, 4 PerfectInterpolantSequences, 212/241 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
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:21,435 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...
sat
