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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:13,672 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:13,774 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f9c47fcd-76f4-4ab7-8d56-2d4073f04971/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:13,781 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:13,783 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:13,820 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:13,821 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:13,821 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:13,823 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:13,823 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:13,824 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:13,825 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:13,825 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:13,825 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:13,825 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:13,825 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:13,825 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:13,826 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:13,826 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,826 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:13,826 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:13,827 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:13,827 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:13,827 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:13,827 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:13,828 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:13,828 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:14,161 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:14,173 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:14,176 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:14,180 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:14,180 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:14,182 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f9c47fcd-76f4-4ab7-8d56-2d4073f04971/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-223.smt2
[2025-04-28 21:21:14,187 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:14,190 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,484 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f9c47fcd-76f4-4ab7-8d56-2d4073f04971/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-223.smt2
[2025-04-28 21:21:14,488 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:14,489 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:14,490 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:14,490 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:14,491 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:14,493 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,519 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,520 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:14,521 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,521 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:14,521 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:14,537 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,537 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,558 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,558 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,561 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,562 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,564 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,565 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,566 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,580 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,581 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:14,582 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:14,582 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:14,583 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,585 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,602 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,618 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,634 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:14,635 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:14,635 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:14,635 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main15 given in one single declaration
[2025-04-28 21:21:14,635 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main15
[2025-04-28 21:21:14,635 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main15
[2025-04-28 21:21:14,635 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd_post given in one single declaration
[2025-04-28 21:21:14,635 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd_post
[2025-04-28 21:21:14,635 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd_post
[2025-04-28 21:21:14,636 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd1 given in one single declaration
[2025-04-28 21:21:14,636 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd1
[2025-04-28 21:21:14,636 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd1
[2025-04-28 21:21:14,636 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd12 given in one single declaration
[2025-04-28 21:21:14,636 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd12
[2025-04-28 21:21:14,636 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd12
[2025-04-28 21:21:14,636 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd10 given in one single declaration
[2025-04-28 21:21:14,636 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd10
[2025-04-28 21:21:14,636 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd10
[2025-04-28 21:21:14,636 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd6 given in one single declaration
[2025-04-28 21:21:14,637 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd6
[2025-04-28 21:21:14,637 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd6
[2025-04-28 21:21:14,637 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd8 given in one single declaration
[2025-04-28 21:21:14,637 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd8
[2025-04-28 21:21:14,637 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd8
[2025-04-28 21:21:14,637 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd3 given in one single declaration
[2025-04-28 21:21:14,637 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd3
[2025-04-28 21:21:14,637 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd3
[2025-04-28 21:21:14,637 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd5 given in one single declaration
[2025-04-28 21:21:14,637 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd5
[2025-04-28 21:21:14,637 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd5
[2025-04-28 21:21:14,637 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd0 given in one single declaration
[2025-04-28 21:21:14,638 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd0
[2025-04-28 21:21:14,638 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd0
[2025-04-28 21:21:14,638 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd_pre given in one single declaration
[2025-04-28 21:21:14,638 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd_pre
[2025-04-28 21:21:14,638 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd_pre
[2025-04-28 21:21:14,638 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd13 given in one single declaration
[2025-04-28 21:21:14,638 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd13
[2025-04-28 21:21:14,638 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd13
[2025-04-28 21:21:14,638 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd9 given in one single declaration
[2025-04-28 21:21:14,638 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd9
[2025-04-28 21:21:14,638 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd9
[2025-04-28 21:21:14,639 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd11 given in one single declaration
[2025-04-28 21:21:14,639 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd11
[2025-04-28 21:21:14,639 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd11
[2025-04-28 21:21:14,639 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd4 given in one single declaration
[2025-04-28 21:21:14,639 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd4
[2025-04-28 21:21:14,639 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd4
[2025-04-28 21:21:14,639 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure gcd7 given in one single declaration
[2025-04-28 21:21:14,639 INFO  L130     BoogieDeclarations]: Found specification of procedure gcd7
[2025-04-28 21:21:14,639 INFO  L138     BoogieDeclarations]: Found implementation of procedure gcd7
[2025-04-28 21:21:14,639 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main13 given in one single declaration
[2025-04-28 21:21:14,639 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main13
[2025-04-28 21:21:14,639 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main13
[2025-04-28 21:21:14,640 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main2 given in one single declaration
[2025-04-28 21:21:14,640 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main2
[2025-04-28 21:21:14,640 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main2
[2025-04-28 21:21:14,640 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:14,640 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:14,640 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:14,709 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:14,712 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:14,927 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:14,928 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:14,946 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:14,947 INFO  L312             CfgBuilder]: Removed 11 assume(true) statements.
[2025-04-28 21:21:14,948 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,948 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:14,951 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:14,951 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:14,955 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:14,955 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:14,956 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@25a6f6a1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,956 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:14,957 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@25a6f6a1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,957 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:14,959 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:14,976 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:14,978 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 20 procedures, 77 locations, 116 edges, 20 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:15,029 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:15,052 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;@70b8eaf2, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:15,052 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:15,057 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 77 states, 33 states have (on average 1.0606060606060606) internal successors, (35), 35 states have internal predecessors, (35), 24 states have call successors, (27), 19 states have call predecessors, (27), 19 states have return successors, (27), 22 states have call predecessors, (27), 24 states have call successors, (27)
[2025-04-28 21:21:15,068 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:15,068 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,069 INFO  L218           NwaCegarLoop]: trace histogram [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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,070 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,076 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,077 INFO  L85        PathProgramCache]: Analyzing trace with hash -1129537944, now seen corresponding path program 1 times
[2025-04-28 21:21:15,085 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,086 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [317345419]
[2025-04-28 21:21:15,086 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,086 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,122 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:15,161 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:15,161 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,162 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,109 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 3 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:16,110 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,110 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [317345419]
[2025-04-28 21:21:16,111 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [317345419] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:16,111 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1142991877]
[2025-04-28 21:21:16,111 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,112 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:16,115 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,119 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,121 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,181 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:16,216 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:16,217 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,217 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,224 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:16,232 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:16,658 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 3 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:16,658 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:19,559 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 3 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:19,560 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1142991877] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:19,560 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:19,563 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 16
[2025-04-28 21:21:19,568 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1114379041]
[2025-04-28 21:21:19,568 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,573 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:19,574 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,610 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:19,614 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=201, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:19,618 INFO  L87              Difference]: Start difference. First operand  has 77 states, 33 states have (on average 1.0606060606060606) internal successors, (35), 35 states have internal predecessors, (35), 24 states have call successors, (27), 19 states have call predecessors, (27), 19 states have return successors, (27), 22 states have call predecessors, (27), 24 states have call successors, (27) Second operand  has 16 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 14 states have internal predecessors, (26), 11 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (19), 13 states have call predecessors, (19), 11 states have call successors, (19)
[2025-04-28 21:21:19,899 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,899 INFO  L93              Difference]: Finished difference Result 79 states and 92 transitions.
[2025-04-28 21:21:19,903 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:19,905 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 14 states have internal predecessors, (26), 11 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (19), 13 states have call predecessors, (19), 11 states have call successors, (19) Word has length 40
[2025-04-28 21:21:19,905 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,914 INFO  L225             Difference]: With dead ends: 79
[2025-04-28 21:21:19,914 INFO  L226             Difference]: Without dead ends: 79
[2025-04-28 21:21:19,917 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 90 GetRequests, 75 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 30 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=43, Invalid=229, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:19,923 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 1 mSDsluCounter, 745 mSDsCounter, 0 mSdLazyCounter, 110 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 823 SdHoareTripleChecker+Invalid, 110 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 110 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,924 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 823 Invalid, 110 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 110 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:19,940 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 79 states.
[2025-04-28 21:21:19,972 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 79 to 79.
[2025-04-28 21:21:19,974 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 34 states have (on average 1.0294117647058822) internal successors, (35), 35 states have internal predecessors, (35), 24 states have call successors, (27), 19 states have call predecessors, (27), 21 states have return successors, (30), 24 states have call predecessors, (30), 24 states have call successors, (30)
[2025-04-28 21:21:19,982 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 92 transitions.
[2025-04-28 21:21:19,983 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 92 transitions. Word has length 40
[2025-04-28 21:21:19,984 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,985 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 92 transitions.
[2025-04-28 21:21:19,985 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 14 states have internal predecessors, (26), 11 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (19), 13 states have call predecessors, (19), 11 states have call successors, (19)
[2025-04-28 21:21:19,985 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 92 transitions.
[2025-04-28 21:21:19,990 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 48
[2025-04-28 21:21:19,990 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,990 INFO  L218           NwaCegarLoop]: trace histogram [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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,997 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:20,191 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,191 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,192 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,194 INFO  L85        PathProgramCache]: Analyzing trace with hash 448931803, now seen corresponding path program 1 times
[2025-04-28 21:21:20,194 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,194 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1328495993]
[2025-04-28 21:21:20,194 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,194 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,207 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 47 statements into 1 equivalence classes.
[2025-04-28 21:21:20,216 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 47 of 47 statements.
[2025-04-28 21:21:20,220 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,220 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,421 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:20,422 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,422 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1328495993]
[2025-04-28 21:21:20,422 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1328495993] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,422 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,422 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:20,423 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1718091639]
[2025-04-28 21:21:20,423 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,425 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:20,425 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,426 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:20,426 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:20,427 INFO  L87              Difference]: Start difference. First operand 79 states and 92 transitions. Second operand  has 9 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 9 states have internal predecessors, (18), 4 states have call successors, (12), 1 states have call predecessors, (12), 7 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:20,572 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,572 INFO  L93              Difference]: Finished difference Result 86 states and 101 transitions.
[2025-04-28 21:21:20,573 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:20,573 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 9 states have internal predecessors, (18), 4 states have call successors, (12), 1 states have call predecessors, (12), 7 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12) Word has length 47
[2025-04-28 21:21:20,573 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,574 INFO  L225             Difference]: With dead ends: 86
[2025-04-28 21:21:20,576 INFO  L226             Difference]: Without dead ends: 74
[2025-04-28 21:21:20,576 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:20,578 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 2 mSDsluCounter, 568 mSDsCounter, 0 mSdLazyCounter, 72 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 653 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 72 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,579 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 653 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 72 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:20,580 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-04-28 21:21:20,592 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 74.
[2025-04-28 21:21:20,596 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 74 states, 32 states have (on average 1.0) internal successors, (32), 32 states have internal predecessors, (32), 22 states have call successors, (25), 18 states have call predecessors, (25), 20 states have return successors, (28), 23 states have call predecessors, (28), 22 states have call successors, (28)
[2025-04-28 21:21:20,597 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 74 states to 74 states and 85 transitions.
[2025-04-28 21:21:20,597 INFO  L79                 Accepts]: Start accepts. Automaton has 74 states and 85 transitions. Word has length 47
[2025-04-28 21:21:20,598 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,598 INFO  L485      AbstractCegarLoop]: Abstraction has 74 states and 85 transitions.
[2025-04-28 21:21:20,598 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 9 states have internal predecessors, (18), 4 states have call successors, (12), 1 states have call predecessors, (12), 7 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:20,599 INFO  L278                IsEmpty]: Start isEmpty. Operand 74 states and 85 transitions.
[2025-04-28 21:21:20,601 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 86
[2025-04-28 21:21:20,603 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,604 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 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, 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,604 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:20,604 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,605 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,605 INFO  L85        PathProgramCache]: Analyzing trace with hash -1904718070, now seen corresponding path program 1 times
[2025-04-28 21:21:20,605 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,605 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1376616674]
[2025-04-28 21:21:20,605 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,605 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,619 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 85 statements into 1 equivalence classes.
[2025-04-28 21:21:20,634 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 85 of 85 statements.
[2025-04-28 21:21:20,636 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,637 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,887 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 3 proven. 7 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:20,887 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,887 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1376616674]
[2025-04-28 21:21:20,888 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1376616674] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:20,888 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1785620850]
[2025-04-28 21:21:20,888 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,888 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,891 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,894 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:20,898 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:20,970 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 85 statements into 1 equivalence classes.
[2025-04-28 21:21:21,019 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 85 of 85 statements.
[2025-04-28 21:21:21,019 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,019 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,024 INFO  L256         TraceCheckSpWp]: Trace formula consists of 297 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:21,027 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,109 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 22 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:21,109 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:21,109 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1785620850] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,109 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:21,109 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6] total 7
[2025-04-28 21:21:21,109 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1411971492]
[2025-04-28 21:21:21,109 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,110 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:21,110 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,112 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:21,112 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,113 INFO  L87              Difference]: Start difference. First operand 74 states and 85 transitions. Second operand  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (23), 2 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-04-28 21:21:21,176 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,178 INFO  L93              Difference]: Finished difference Result 78 states and 89 transitions.
[2025-04-28 21:21:21,180 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:21,180 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (23), 2 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23) Word has length 85
[2025-04-28 21:21:21,181 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,182 INFO  L225             Difference]: With dead ends: 78
[2025-04-28 21:21:21,182 INFO  L226             Difference]: Without dead ends: 78
[2025-04-28 21:21:21,182 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 90 GetRequests, 85 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,183 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 1 mSDsluCounter, 288 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 363 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,183 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 363 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:21,185 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-04-28 21:21:21,195 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-04-28 21:21:21,197 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 34 states have (on average 1.0) internal successors, (34), 34 states have internal predecessors, (34), 22 states have call successors, (25), 18 states have call predecessors, (25), 22 states have return successors, (30), 25 states have call predecessors, (30), 22 states have call successors, (30)
[2025-04-28 21:21:21,199 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 89 transitions.
[2025-04-28 21:21:21,201 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 89 transitions. Word has length 85
[2025-04-28 21:21:21,201 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,201 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 89 transitions.
[2025-04-28 21:21:21,201 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 6.8) internal successors, (34), 6 states have internal predecessors, (34), 4 states have call successors, (23), 2 states have call predecessors, (23), 5 states have return successors, (23), 5 states have call predecessors, (23), 4 states have call successors, (23)
[2025-04-28 21:21:21,202 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 89 transitions.
[2025-04-28 21:21:21,207 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 112
[2025-04-28 21:21:21,207 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,208 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,214 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:21,408 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,408 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,409 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,409 INFO  L85        PathProgramCache]: Analyzing trace with hash -71356254, now seen corresponding path program 1 times
[2025-04-28 21:21:21,409 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,409 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [224428867]
[2025-04-28 21:21:21,410 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,410 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,426 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-04-28 21:21:21,444 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-04-28 21:21:21,444 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,444 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,422 INFO  L134       CoverageAnalysis]: Checked inductivity of 67 backedges. 9 proven. 24 refuted. 0 times theorem prover too weak. 34 trivial. 0 not checked.
[2025-04-28 21:21:22,423 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,423 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [224428867]
[2025-04-28 21:21:22,423 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [224428867] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,423 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [869702025]
[2025-04-28 21:21:22,423 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,423 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,425 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,428 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:22,431 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,499 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 111 statements into 1 equivalence classes.
[2025-04-28 21:21:22,554 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 111 of 111 statements.
[2025-04-28 21:21:22,554 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,554 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,556 INFO  L256         TraceCheckSpWp]: Trace formula consists of 393 conjuncts, 26 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,565 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,071 INFO  L134       CoverageAnalysis]: Checked inductivity of 67 backedges. 9 proven. 16 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:21:23,071 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,451 INFO  L134       CoverageAnalysis]: Checked inductivity of 67 backedges. 9 proven. 16 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:21:28,451 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [869702025] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,451 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,451 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [22, 16, 16] total 36
[2025-04-28 21:21:28,451 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1500822489]
[2025-04-28 21:21:28,452 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,452 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 36 states
[2025-04-28 21:21:28,453 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,454 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 36 interpolants.
[2025-04-28 21:21:28,454 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=90, Invalid=1170, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:21:28,455 INFO  L87              Difference]: Start difference. First operand 78 states and 89 transitions. Second operand  has 36 states, 25 states have (on average 2.4) internal successors, (60), 33 states have internal predecessors, (60), 18 states have call successors, (34), 1 states have call predecessors, (34), 25 states have return successors, (47), 28 states have call predecessors, (47), 18 states have call successors, (47)
[2025-04-28 21:21:29,126 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,126 INFO  L93              Difference]: Finished difference Result 80 states and 90 transitions.
[2025-04-28 21:21:29,126 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-04-28 21:21:29,127 INFO  L79                 Accepts]: Start accepts. Automaton has  has 36 states, 25 states have (on average 2.4) internal successors, (60), 33 states have internal predecessors, (60), 18 states have call successors, (34), 1 states have call predecessors, (34), 25 states have return successors, (47), 28 states have call predecessors, (47), 18 states have call successors, (47) Word has length 111
[2025-04-28 21:21:29,128 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,130 INFO  L225             Difference]: With dead ends: 80
[2025-04-28 21:21:29,130 INFO  L226             Difference]: Without dead ends: 80
[2025-04-28 21:21:29,131 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 250 GetRequests, 206 SyntacticMatches, 3 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 265 ImplicationChecksByTransitivity, 1.0s TimeCoverageRelationStatistics Valid=123, Invalid=1683, Unknown=0, NotChecked=0, Total=1806
[2025-04-28 21:21:29,132 INFO  L437           NwaCegarLoop]: 65 mSDtfsCounter, 4 mSDsluCounter, 1672 mSDsCounter, 0 mSdLazyCounter, 500 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 1737 SdHoareTripleChecker+Invalid, 502 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 500 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,133 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 1737 Invalid, 502 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 500 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:29,133 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 80 states.
[2025-04-28 21:21:29,145 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 80 to 78.
[2025-04-28 21:21:29,146 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 34 states have (on average 1.0) internal successors, (34), 34 states have internal predecessors, (34), 22 states have call successors, (25), 18 states have call predecessors, (25), 22 states have return successors, (29), 25 states have call predecessors, (29), 22 states have call successors, (29)
[2025-04-28 21:21:29,147 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 88 transitions.
[2025-04-28 21:21:29,147 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 88 transitions. Word has length 111
[2025-04-28 21:21:29,147 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,148 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 88 transitions.
[2025-04-28 21:21:29,148 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 36 states, 25 states have (on average 2.4) internal successors, (60), 33 states have internal predecessors, (60), 18 states have call successors, (34), 1 states have call predecessors, (34), 25 states have return successors, (47), 28 states have call predecessors, (47), 18 states have call successors, (47)
[2025-04-28 21:21:29,148 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 88 transitions.
[2025-04-28 21:21:29,150 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 115
[2025-04-28 21:21:29,150 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,150 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 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, 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:29,155 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:29,353 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,353 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,354 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,354 INFO  L85        PathProgramCache]: Analyzing trace with hash 1138021255, now seen corresponding path program 1 times
[2025-04-28 21:21:29,354 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,354 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1124040922]
[2025-04-28 21:21:29,354 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,354 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,365 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 114 statements into 1 equivalence classes.
[2025-04-28 21:21:29,376 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 114 of 114 statements.
[2025-04-28 21:21:29,376 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,376 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,825 INFO  L134       CoverageAnalysis]: Checked inductivity of 59 backedges. 4 proven. 13 refuted. 0 times theorem prover too weak. 42 trivial. 0 not checked.
[2025-04-28 21:21:29,826 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,826 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1124040922]
[2025-04-28 21:21:29,826 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1124040922] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,826 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [951774300]
[2025-04-28 21:21:29,826 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,826 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,829 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,831 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,836 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,950 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 114 statements into 1 equivalence classes.
[2025-04-28 21:21:30,009 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 114 of 114 statements.
[2025-04-28 21:21:30,009 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,010 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,017 INFO  L256         TraceCheckSpWp]: Trace formula consists of 405 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,024 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,140 INFO  L134       CoverageAnalysis]: Checked inductivity of 59 backedges. 44 proven. 0 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:30,140 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:30,141 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [951774300] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,141 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:30,141 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [13] total 15
[2025-04-28 21:21:30,141 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [975849888]
[2025-04-28 21:21:30,141 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,142 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:30,142 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,142 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:30,143 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=180, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:30,143 INFO  L87              Difference]: Start difference. First operand 78 states and 88 transitions. Second operand  has 13 states, 10 states have (on average 4.4) internal successors, (44), 13 states have internal predecessors, (44), 6 states have call successors, (29), 2 states have call predecessors, (29), 10 states have return successors, (30), 10 states have call predecessors, (30), 6 states have call successors, (30)
[2025-04-28 21:21:30,290 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,290 INFO  L93              Difference]: Finished difference Result 82 states and 92 transitions.
[2025-04-28 21:21:30,292 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:30,293 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 10 states have (on average 4.4) internal successors, (44), 13 states have internal predecessors, (44), 6 states have call successors, (29), 2 states have call predecessors, (29), 10 states have return successors, (30), 10 states have call predecessors, (30), 6 states have call successors, (30) Word has length 114
[2025-04-28 21:21:30,293 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,294 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:21:30,294 INFO  L226             Difference]: Without dead ends: 82
[2025-04-28 21:21:30,295 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 127 GetRequests, 112 SyntacticMatches, 1 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=34, Invalid=206, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:30,296 INFO  L437           NwaCegarLoop]: 73 mSDtfsCounter, 2 mSDsluCounter, 697 mSDsCounter, 0 mSdLazyCounter, 130 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 770 SdHoareTripleChecker+Invalid, 130 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 130 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,296 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 770 Invalid, 130 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 130 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,297 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-04-28 21:21:30,309 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 78.
[2025-04-28 21:21:30,310 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 34 states have (on average 1.0) internal successors, (34), 34 states have internal predecessors, (34), 22 states have call successors, (25), 18 states have call predecessors, (25), 22 states have return successors, (29), 25 states have call predecessors, (29), 22 states have call successors, (29)
[2025-04-28 21:21:30,311 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 88 transitions.
[2025-04-28 21:21:30,311 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 88 transitions. Word has length 114
[2025-04-28 21:21:30,311 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,311 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 88 transitions.
[2025-04-28 21:21:30,311 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 10 states have (on average 4.4) internal successors, (44), 13 states have internal predecessors, (44), 6 states have call successors, (29), 2 states have call predecessors, (29), 10 states have return successors, (30), 10 states have call predecessors, (30), 6 states have call successors, (30)
[2025-04-28 21:21:30,312 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 88 transitions.
[2025-04-28 21:21:30,315 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 118
[2025-04-28 21:21:30,319 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,319 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,326 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:30,519 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:30,520 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,520 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,520 INFO  L85        PathProgramCache]: Analyzing trace with hash -601651316, now seen corresponding path program 1 times
[2025-04-28 21:21:30,520 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,520 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1343561584]
[2025-04-28 21:21:30,520 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,520 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,529 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 117 statements into 1 equivalence classes.
[2025-04-28 21:21:30,550 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 117 of 117 statements.
[2025-04-28 21:21:30,550 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,550 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,112 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 12 proven. 27 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:32,112 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,112 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1343561584]
[2025-04-28 21:21:32,113 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1343561584] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,113 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [227264404]
[2025-04-28 21:21:32,113 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,113 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,115 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,117 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:32,122 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,230 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 117 statements into 1 equivalence classes.
[2025-04-28 21:21:32,289 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 117 of 117 statements.
[2025-04-28 21:21:32,289 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,289 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,292 INFO  L256         TraceCheckSpWp]: Trace formula consists of 417 conjuncts, 52 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,296 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,748 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 9 proven. 23 refuted. 0 times theorem prover too weak. 38 trivial. 0 not checked.
[2025-04-28 21:21:32,748 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,778 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 9 proven. 23 refuted. 0 times theorem prover too weak. 38 trivial. 0 not checked.
[2025-04-28 21:21:44,778 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [227264404] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,779 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,779 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [29, 25, 25] total 45
[2025-04-28 21:21:44,779 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [779879860]
[2025-04-28 21:21:44,779 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,779 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 45 states
[2025-04-28 21:21:44,780 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,780 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 45 interpolants.
[2025-04-28 21:21:44,782 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=123, Invalid=1857, Unknown=0, NotChecked=0, Total=1980
[2025-04-28 21:21:44,782 INFO  L87              Difference]: Start difference. First operand 78 states and 88 transitions. Second operand  has 45 states, 32 states have (on average 1.96875) internal successors, (63), 43 states have internal predecessors, (63), 18 states have call successors, (34), 1 states have call predecessors, (34), 32 states have return successors, (51), 34 states have call predecessors, (51), 18 states have call successors, (51)
[2025-04-28 21:21:45,495 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,496 INFO  L93              Difference]: Finished difference Result 68 states and 76 transitions.
[2025-04-28 21:21:45,496 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-04-28 21:21:45,497 INFO  L79                 Accepts]: Start accepts. Automaton has  has 45 states, 32 states have (on average 1.96875) internal successors, (63), 43 states have internal predecessors, (63), 18 states have call successors, (34), 1 states have call predecessors, (34), 32 states have return successors, (51), 34 states have call predecessors, (51), 18 states have call successors, (51) Word has length 117
[2025-04-28 21:21:45,497 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,497 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:45,497 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:45,499 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 275 GetRequests, 219 SyntacticMatches, 6 SemanticMatches, 50 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 340 ImplicationChecksByTransitivity, 1.4s TimeCoverageRelationStatistics Valid=164, Invalid=2488, Unknown=0, NotChecked=0, Total=2652
[2025-04-28 21:21:45,499 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 2 mSDsluCounter, 1570 mSDsCounter, 0 mSdLazyCounter, 514 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 1629 SdHoareTripleChecker+Invalid, 515 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 514 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,500 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 1629 Invalid, 515 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 514 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:45,500 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:45,500 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:45,501 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:45,501 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:45,501 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 117
[2025-04-28 21:21:45,501 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,501 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:45,501 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 45 states, 32 states have (on average 1.96875) internal successors, (63), 43 states have internal predecessors, (63), 18 states have call successors, (34), 1 states have call predecessors, (34), 32 states have return successors, (51), 34 states have call predecessors, (51), 18 states have call successors, (51)
[2025-04-28 21:21:45,501 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:45,501 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:45,504 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:45,511 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:45,705 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,709 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,711 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:45,715 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:45 BoogieIcfgContainer
[2025-04-28 21:21:45,715 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:45,716 INFO  L158              Benchmark]: Toolchain (without parser) took 31226.63ms. Allocated memory was 234.9MB in the beginning and 268.4MB in the end (delta: 33.6MB). Free memory was 164.4MB in the beginning and 209.4MB in the end (delta: -45.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:45,716 INFO  L158              Benchmark]: SmtParser took 3.48ms. Allocated memory is still 234.9MB. Free memory is still 173.3MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:45,716 INFO  L158              Benchmark]: ChcToBoogie took 29.89ms. Allocated memory is still 234.9MB. Free memory was 164.4MB in the beginning and 163.4MB in the end (delta: 1.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:45,717 INFO  L158              Benchmark]: Boogie Preprocessor took 60.04ms. Allocated memory is still 234.9MB. Free memory was 163.4MB in the beginning and 161.0MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:45,717 INFO  L158              Benchmark]: RCFGBuilder took 366.59ms. Allocated memory is still 234.9MB. Free memory was 161.0MB in the beginning and 149.2MB in the end (delta: 11.8MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:45,717 INFO  L158              Benchmark]: TraceAbstraction took 30764.33ms. Allocated memory was 234.9MB in the beginning and 268.4MB in the end (delta: 33.6MB). Free memory was 148.6MB in the beginning and 209.4MB in the end (delta: -60.9MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:45,719 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 3.48ms. Allocated memory is still 234.9MB. Free memory is still 173.3MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 29.89ms. Allocated memory is still 234.9MB. Free memory was 164.4MB in the beginning and 163.4MB in the end (delta: 1.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 60.04ms. Allocated memory is still 234.9MB. Free memory was 163.4MB in the beginning and 161.0MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 366.59ms. Allocated memory is still 234.9MB. Free memory was 161.0MB in the beginning and 149.2MB in the end (delta: 11.8MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 30764.33ms. Allocated memory was 234.9MB in the beginning and 268.4MB in the end (delta: 33.6MB). Free memory was 148.6MB in the beginning and 209.4MB in the end (delta: -60.9MB). 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
  - 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 20 procedures, 77 locations, 116 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 30.7s, OverallIterations: 6, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 2.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 22 SdHoareTripleChecker+Valid, 1.4s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 12 mSDsluCounter, 5975 SdHoareTripleChecker+Invalid, 1.1s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 5540 mSDsCounter, 5 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1356 IncrementalHoareTripleChecker+Invalid, 1361 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 5 mSolverCounterUnsat, 435 mSDtfsCounter, 1356 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 842 GetRequests, 699 SyntacticMatches, 10 SemanticMatches, 133 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 644 ImplicationChecksByTransitivity, 3.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=79occurred in iteration=1, InterpolantAutomatonStates: 82, 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, 6 MinimizatonAttempts, 6 StatesRemovedByMinimization, 2 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 26.3s InterpolantComputationTime, 981 NumberOfCodeBlocks, 981 NumberOfCodeBlocksAsserted, 11 NumberOfCheckSat, 1235 ConstructedInterpolants, 0 QuantifiedInterpolants, 3072 SizeOfPredicates, 34 NumberOfNonLiveVariables, 1642 ConjunctsInSsa, 126 ConjunctsInUnsatCore, 14 InterpolantComputations, 3 PerfectInterpolantSequences, 457/615 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:45,739 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
