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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:10,914 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:11,007 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_63c8b9fc-0246-458e-b64b-494b6b827902/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:11,017 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:11,017 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:11,054 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:11,055 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:11,055 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:11,055 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:11,055 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:11,056 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:11,056 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:11,056 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:11,056 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:11,056 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:11,057 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:11,057 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:11,058 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:11,058 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:11,059 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:11,059 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:11,378 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:11,387 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:11,390 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:11,391 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:11,391 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:11,393 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_63c8b9fc-0246-458e-b64b-494b6b827902/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-040.smt2
[2025-04-28 21:21:11,394 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:11,398 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:11,870 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_63c8b9fc-0246-458e-b64b-494b6b827902/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-040.smt2
[2025-04-28 21:21:11,873 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:11,879 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:11,880 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:11,880 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:11,880 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:11,883 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,932 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11 Unit
[2025-04-28 21:21:11,933 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:11,937 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:11,937 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:11,938 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:11,955 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,955 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:11,999 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,002 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,013 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,018 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,021 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,027 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,028 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,053 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,054 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:12,054 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:12,054 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:12,055 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (1/1) ...
[2025-04-28 21:21:12,058 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:12,071 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:12,084 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:12,087 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:12,103 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:12,103 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:12,103 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:12,103 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:12,103 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:12,103 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:12,103 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:12,103 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:12,103 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__sem given in one single declaration
[2025-04-28 21:21:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__sem
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__sem
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__sem given in one single declaration
[2025-04-28 21:21:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__sem
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__sem
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcA__sem given in one single declaration
[2025-04-28 21:21:12,104 INFO  L130     BoogieDeclarations]: Found specification of procedure funcA__sem
[2025-04-28 21:21:12,104 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcA__sem
[2025-04-28 21:21:12,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__sem given in one single declaration
[2025-04-28 21:21:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__sem
[2025-04-28 21:21:12,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__sem
[2025-04-28 21:21:12,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__syn given in one single declaration
[2025-04-28 21:21:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__syn
[2025-04-28 21:21:12,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__syn
[2025-04-28 21:21:12,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:12,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:12,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcA__syn given in one single declaration
[2025-04-28 21:21:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure funcA__syn
[2025-04-28 21:21:12,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcA__syn
[2025-04-28 21:21:12,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__syn given in one single declaration
[2025-04-28 21:21:12,105 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__syn
[2025-04-28 21:21:12,106 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__syn
[2025-04-28 21:21:12,106 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:12,106 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:12,106 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:12,258 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:12,260 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:12,704 INFO  L?                        ?]: Removed 48 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:12,704 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:12,723 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:12,723 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:12,724 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12 BoogieIcfgContainer
[2025-04-28 21:21:12,724 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:12,726 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:12,728 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:12,733 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:12,733 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:11" (1/3) ...
[2025-04-28 21:21:12,734 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@54237af7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,735 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:11" (2/3) ...
[2025-04-28 21:21:12,735 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@54237af7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,735 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12" (3/3) ...
[2025-04-28 21:21:12,736 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:12,755 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:12,757 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 13 procedures, 70 locations, 132 edges, 13 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:12,806 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:12,818 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;@637259be, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:12,818 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:12,822 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 70 states, 25 states have (on average 1.56) internal successors, (39), 35 states have internal predecessors, (39), 31 states have call successors, (31), 12 states have call predecessors, (31), 12 states have return successors, (31), 23 states have call predecessors, (31), 31 states have call successors, (31)
[2025-04-28 21:21:12,834 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:12,834 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:12,835 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 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:12,836 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:12,842 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:12,842 INFO  L85        PathProgramCache]: Analyzing trace with hash -119450341, now seen corresponding path program 1 times
[2025-04-28 21:21:12,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:12,850 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [880048287]
[2025-04-28 21:21:12,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:12,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:12,921 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:13,087 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:13,088 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,088 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:13,996 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:13,997 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:13,997 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [880048287]
[2025-04-28 21:21:13,998 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [880048287] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:13,998 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,036 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:14,038 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1012787656]
[2025-04-28 21:21:14,043 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,048 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:14,048 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,089 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:14,090 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:14,093 INFO  L87              Difference]: Start difference. First operand  has 70 states, 25 states have (on average 1.56) internal successors, (39), 35 states have internal predecessors, (39), 31 states have call successors, (31), 12 states have call predecessors, (31), 12 states have return successors, (31), 23 states have call predecessors, (31), 31 states have call successors, (31) Second operand  has 6 states, 4 states have (on average 4.0) internal successors, (16), 6 states have internal predecessors, (16), 3 states have call successors, (11), 1 states have call predecessors, (11), 4 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:14,312 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,313 INFO  L93              Difference]: Finished difference Result 72 states and 103 transitions.
[2025-04-28 21:21:14,314 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:14,316 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 4.0) internal successors, (16), 6 states have internal predecessors, (16), 3 states have call successors, (11), 1 states have call predecessors, (11), 4 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11) Word has length 44
[2025-04-28 21:21:14,317 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,326 INFO  L225             Difference]: With dead ends: 72
[2025-04-28 21:21:14,326 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:21:14,332 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:14,338 INFO  L437           NwaCegarLoop]: 96 mSDtfsCounter, 2 mSDsluCounter, 369 mSDsCounter, 0 mSdLazyCounter, 21 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 465 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:14,340 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 465 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:14,355 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:21:14,379 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-04-28 21:21:14,380 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 25 states have (on average 1.52) internal successors, (38), 34 states have internal predecessors, (38), 31 states have call successors, (31), 12 states have call predecessors, (31), 13 states have return successors, (32), 23 states have call predecessors, (32), 31 states have call successors, (32)
[2025-04-28 21:21:14,385 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 101 transitions.
[2025-04-28 21:21:14,387 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 101 transitions. Word has length 44
[2025-04-28 21:21:14,388 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,389 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 101 transitions.
[2025-04-28 21:21:14,389 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 4.0) internal successors, (16), 6 states have internal predecessors, (16), 3 states have call successors, (11), 1 states have call predecessors, (11), 4 states have return successors, (11), 4 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:14,389 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 101 transitions.
[2025-04-28 21:21:14,393 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:21:14,393 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,393 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 4, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,393 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:14,394 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,394 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,394 INFO  L85        PathProgramCache]: Analyzing trace with hash 2134046473, now seen corresponding path program 1 times
[2025-04-28 21:21:14,395 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,395 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [280138522]
[2025-04-28 21:21:14,395 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,395 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,460 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:14,588 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:14,588 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,588 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,525 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:15,525 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,526 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [280138522]
[2025-04-28 21:21:15,526 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [280138522] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:15,526 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [577303981]
[2025-04-28 21:21:15,526 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,526 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:15,531 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:15,534 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:15,536 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:15,757 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:15,990 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:15,991 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,999 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1026 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:16,008 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:16,237 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:16,237 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:17,772 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:17,773 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [577303981] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:17,773 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:17,773 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 10, 10] total 13
[2025-04-28 21:21:17,774 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1737526067]
[2025-04-28 21:21:17,774 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,775 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:17,776 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,777 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:17,777 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=125, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:17,777 INFO  L87              Difference]: Start difference. First operand 70 states and 101 transitions. Second operand  has 13 states, 7 states have (on average 4.714285714285714) internal successors, (33), 12 states have internal predecessors, (33), 8 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (23), 5 states have call predecessors, (23), 8 states have call successors, (23)
[2025-04-28 21:21:18,008 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,010 INFO  L93              Difference]: Finished difference Result 81 states and 120 transitions.
[2025-04-28 21:21:18,011 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:18,011 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 4.714285714285714) internal successors, (33), 12 states have internal predecessors, (33), 8 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (23), 5 states have call predecessors, (23), 8 states have call successors, (23) Word has length 76
[2025-04-28 21:21:18,012 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,013 INFO  L225             Difference]: With dead ends: 81
[2025-04-28 21:21:18,014 INFO  L226             Difference]: Without dead ends: 75
[2025-04-28 21:21:18,015 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 162 GetRequests, 147 SyntacticMatches, 3 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 30 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=36, Invalid=146, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:18,016 INFO  L437           NwaCegarLoop]: 93 mSDtfsCounter, 5 mSDsluCounter, 529 mSDsCounter, 0 mSdLazyCounter, 79 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 622 SdHoareTripleChecker+Invalid, 82 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 79 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,016 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 622 Invalid, 82 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 79 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:18,017 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 75 states.
[2025-04-28 21:21:18,030 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 75 to 73.
[2025-04-28 21:21:18,033 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 73 states, 26 states have (on average 1.5) internal successors, (39), 36 states have internal predecessors, (39), 32 states have call successors, (32), 12 states have call predecessors, (32), 14 states have return successors, (39), 24 states have call predecessors, (39), 32 states have call successors, (39)
[2025-04-28 21:21:18,036 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 73 states to 73 states and 110 transitions.
[2025-04-28 21:21:18,038 INFO  L79                 Accepts]: Start accepts. Automaton has 73 states and 110 transitions. Word has length 76
[2025-04-28 21:21:18,038 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,039 INFO  L485      AbstractCegarLoop]: Abstraction has 73 states and 110 transitions.
[2025-04-28 21:21:18,039 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 4.714285714285714) internal successors, (33), 12 states have internal predecessors, (33), 8 states have call successors, (21), 1 states have call predecessors, (21), 7 states have return successors, (23), 5 states have call predecessors, (23), 8 states have call successors, (23)
[2025-04-28 21:21:18,039 INFO  L278                IsEmpty]: Start isEmpty. Operand 73 states and 110 transitions.
[2025-04-28 21:21:18,042 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:21:18,045 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,045 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 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, 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:18,053 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:18,246 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,246 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,247 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,247 INFO  L85        PathProgramCache]: Analyzing trace with hash 1776573476, now seen corresponding path program 1 times
[2025-04-28 21:21:18,247 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,247 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2123566882]
[2025-04-28 21:21:18,247 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,247 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,292 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:18,360 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:18,360 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,360 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,121 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:19,122 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2123566882]
[2025-04-28 21:21:19,122 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2123566882] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:19,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1147443827]
[2025-04-28 21:21:19,122 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,122 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:19,126 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:19,128 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:19,131 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:19,315 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:19,508 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:19,508 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,508 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,514 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1026 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:19,523 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:19,837 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:19,837 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:22,248 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:22,249 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1147443827] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:22,249 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:22,250 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 17
[2025-04-28 21:21:22,250 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [952091572]
[2025-04-28 21:21:22,250 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,250 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:22,253 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,254 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:22,254 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=44, Invalid=228, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:22,254 INFO  L87              Difference]: Start difference. First operand 73 states and 110 transitions. Second operand  has 17 states, 8 states have (on average 4.625) internal successors, (37), 15 states have internal predecessors, (37), 11 states have call successors, (24), 1 states have call predecessors, (24), 8 states have return successors, (26), 6 states have call predecessors, (26), 11 states have call successors, (26)
[2025-04-28 21:21:22,751 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,751 INFO  L93              Difference]: Finished difference Result 86 states and 133 transitions.
[2025-04-28 21:21:22,752 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:22,753 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 4.625) internal successors, (37), 15 states have internal predecessors, (37), 11 states have call successors, (24), 1 states have call predecessors, (24), 8 states have return successors, (26), 6 states have call predecessors, (26), 11 states have call successors, (26) Word has length 76
[2025-04-28 21:21:22,753 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,756 INFO  L225             Difference]: With dead ends: 86
[2025-04-28 21:21:22,759 INFO  L226             Difference]: Without dead ends: 80
[2025-04-28 21:21:22,760 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 165 GetRequests, 144 SyntacticMatches, 2 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 41 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=70, Invalid=350, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:22,761 INFO  L437           NwaCegarLoop]: 97 mSDtfsCounter, 9 mSDsluCounter, 908 mSDsCounter, 0 mSdLazyCounter, 226 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 1005 SdHoareTripleChecker+Invalid, 238 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 226 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,761 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 1005 Invalid, 238 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 226 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:22,762 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 80 states.
[2025-04-28 21:21:22,779 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 80 to 76.
[2025-04-28 21:21:22,780 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 76 states, 27 states have (on average 1.4814814814814814) internal successors, (40), 38 states have internal predecessors, (40), 33 states have call successors, (33), 12 states have call predecessors, (33), 15 states have return successors, (47), 25 states have call predecessors, (47), 33 states have call successors, (47)
[2025-04-28 21:21:22,783 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 76 states to 76 states and 120 transitions.
[2025-04-28 21:21:22,787 INFO  L79                 Accepts]: Start accepts. Automaton has 76 states and 120 transitions. Word has length 76
[2025-04-28 21:21:22,788 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,788 INFO  L485      AbstractCegarLoop]: Abstraction has 76 states and 120 transitions.
[2025-04-28 21:21:22,788 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 4.625) internal successors, (37), 15 states have internal predecessors, (37), 11 states have call successors, (24), 1 states have call predecessors, (24), 8 states have return successors, (26), 6 states have call predecessors, (26), 11 states have call successors, (26)
[2025-04-28 21:21:22,788 INFO  L278                IsEmpty]: Start isEmpty. Operand 76 states and 120 transitions.
[2025-04-28 21:21:22,790 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:21:22,794 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,795 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 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, 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:22,800 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:22,995 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:22,995 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,996 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,996 INFO  L85        PathProgramCache]: Analyzing trace with hash -836473438, now seen corresponding path program 1 times
[2025-04-28 21:21:22,996 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,996 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2131485210]
[2025-04-28 21:21:22,996 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,996 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,027 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:23,071 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:23,072 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,072 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,684 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:23,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,685 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2131485210]
[2025-04-28 21:21:23,685 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2131485210] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:23,685 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1005731226]
[2025-04-28 21:21:23,685 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,685 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:23,688 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:23,690 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:23,694 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:23,869 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:24,022 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:24,022 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,022 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,029 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1026 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,032 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,342 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:24,342 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:26,305 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:26,305 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1005731226] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,305 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,306 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:21:26,306 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1345792441]
[2025-04-28 21:21:26,306 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,306 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:26,307 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,308 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:26,308 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:26,308 INFO  L87              Difference]: Start difference. First operand 76 states and 120 transitions. Second operand  has 22 states, 10 states have (on average 4.1) internal successors, (41), 19 states have internal predecessors, (41), 15 states have call successors, (29), 1 states have call predecessors, (29), 10 states have return successors, (29), 9 states have call predecessors, (29), 15 states have call successors, (29)
[2025-04-28 21:21:26,965 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,965 INFO  L93              Difference]: Finished difference Result 82 states and 127 transitions.
[2025-04-28 21:21:26,966 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:26,966 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 4.1) internal successors, (41), 19 states have internal predecessors, (41), 15 states have call successors, (29), 1 states have call predecessors, (29), 10 states have return successors, (29), 9 states have call predecessors, (29), 15 states have call successors, (29) Word has length 76
[2025-04-28 21:21:26,967 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,968 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:21:26,968 INFO  L226             Difference]: Without dead ends: 75
[2025-04-28 21:21:26,969 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 170 GetRequests, 140 SyntacticMatches, 2 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=102, Invalid=768, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:26,970 INFO  L437           NwaCegarLoop]: 96 mSDtfsCounter, 10 mSDsluCounter, 1728 mSDsCounter, 0 mSdLazyCounter, 344 mSolverCounterSat, 20 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1824 SdHoareTripleChecker+Invalid, 364 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 20 IncrementalHoareTripleChecker+Valid, 344 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,970 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1824 Invalid, 364 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [20 Valid, 344 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:26,971 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 75 states.
[2025-04-28 21:21:26,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 75 to 75.
[2025-04-28 21:21:26,979 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 75 states, 27 states have (on average 1.4814814814814814) internal successors, (40), 38 states have internal predecessors, (40), 32 states have call successors, (32), 12 states have call predecessors, (32), 15 states have return successors, (45), 24 states have call predecessors, (45), 32 states have call successors, (45)
[2025-04-28 21:21:26,981 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 75 states to 75 states and 117 transitions.
[2025-04-28 21:21:26,981 INFO  L79                 Accepts]: Start accepts. Automaton has 75 states and 117 transitions. Word has length 76
[2025-04-28 21:21:26,981 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,981 INFO  L485      AbstractCegarLoop]: Abstraction has 75 states and 117 transitions.
[2025-04-28 21:21:26,981 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 4.1) internal successors, (41), 19 states have internal predecessors, (41), 15 states have call successors, (29), 1 states have call predecessors, (29), 10 states have return successors, (29), 9 states have call predecessors, (29), 15 states have call successors, (29)
[2025-04-28 21:21:26,982 INFO  L278                IsEmpty]: Start isEmpty. Operand 75 states and 117 transitions.
[2025-04-28 21:21:26,983 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 77
[2025-04-28 21:21:26,983 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,983 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 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, 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:26,990 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:27,184 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:27,184 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,184 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,184 INFO  L85        PathProgramCache]: Analyzing trace with hash 8680924, now seen corresponding path program 1 times
[2025-04-28 21:21:27,185 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,185 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1628658394]
[2025-04-28 21:21:27,185 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,185 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,209 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:27,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:27,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,055 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 2 proven. 14 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:29,055 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,055 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1628658394]
[2025-04-28 21:21:29,055 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1628658394] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,055 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [82693706]
[2025-04-28 21:21:29,055 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,056 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,058 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,060 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,064 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,252 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 76 statements into 1 equivalence classes.
[2025-04-28 21:21:29,410 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 76 of 76 statements.
[2025-04-28 21:21:29,410 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,410 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,418 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1026 conjuncts, 42 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,427 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,881 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 2 proven. 20 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:21:30,881 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,287 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 2 proven. 20 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:21:38,287 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [82693706] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,287 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,287 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [23, 25, 25] total 55
[2025-04-28 21:21:38,287 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1072171381]
[2025-04-28 21:21:38,288 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,288 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 55 states
[2025-04-28 21:21:38,288 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,289 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 55 interpolants.
[2025-04-28 21:21:38,291 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=133, Invalid=2837, Unknown=0, NotChecked=0, Total=2970
[2025-04-28 21:21:38,291 INFO  L87              Difference]: Start difference. First operand 75 states and 117 transitions. Second operand  has 55 states, 22 states have (on average 2.6363636363636362) internal successors, (58), 41 states have internal predecessors, (58), 36 states have call successors, (42), 1 states have call predecessors, (42), 22 states have return successors, (42), 28 states have call predecessors, (42), 36 states have call successors, (42)
