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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:12,232 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:12,312 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_864f4d8d-6f1a-4713-b671-00b8979f6a0a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:12,317 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:12,317 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:12,340 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:12,341 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:12,341 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:12,341 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:12,342 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:12,342 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:12,342 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:12,342 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:12,342 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:12,342 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:12,343 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:12,343 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:12,343 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:12,343 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:12,343 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:12,343 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:12,344 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:12,344 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:12,344 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:12,344 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:12,345 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:12,345 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:12,711 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:12,726 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:12,729 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:12,733 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:12,733 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:12,735 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_864f4d8d-6f1a-4713-b671-00b8979f6a0a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-022.smt2
[2025-04-28 21:21:12,738 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:12,746 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:13,023 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_864f4d8d-6f1a-4713-b671-00b8979f6a0a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-022.smt2
[2025-04-28 21:21:13,027 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:13,029 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:13,030 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:13,030 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:13,031 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:13,035 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,073 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13 Unit
[2025-04-28 21:21:13,073 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:13,075 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:13,076 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:13,076 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:13,095 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,095 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,129 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,129 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,132 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,134 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,139 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,140 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,140 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,158 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:13,160 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:13,161 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:13,161 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:13,162 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (1/1) ...
[2025-04-28 21:21:13,165 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,179 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:13,194 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:13,201 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:13,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:13,215 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:13,216 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure sum given in one single declaration
[2025-04-28 21:21:13,216 INFO  L130     BoogieDeclarations]: Found specification of procedure sum
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure sum
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure sum.AT.split given in one single declaration
[2025-04-28 21:21:13,216 INFO  L130     BoogieDeclarations]: Found specification of procedure sum.AT.split
[2025-04-28 21:21:13,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure sum.AT.split
[2025-04-28 21:21:13,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure sum.AT_call given in one single declaration
[2025-04-28 21:21:13,217 INFO  L130     BoogieDeclarations]: Found specification of procedure sum.AT_call
[2025-04-28 21:21:13,217 INFO  L138     BoogieDeclarations]: Found implementation of procedure sum.AT_call
[2025-04-28 21:21:13,217 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:13,217 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:13,217 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:13,217 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:13,217 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:13,217 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:13,271 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:13,273 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:13,428 INFO  L?                        ?]: Removed 15 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:13,428 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:13,444 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:13,445 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:13,445 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:13 BoogieIcfgContainer
[2025-04-28 21:21:13,445 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:13,449 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:13,449 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:13,455 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:13,455 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:13" (1/3) ...
[2025-04-28 21:21:13,456 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4c7c7229 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:13, skipping insertion in model container
[2025-04-28 21:21:13,456 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:13" (2/3) ...
[2025-04-28 21:21:13,457 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4c7c7229 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:13, skipping insertion in model container
[2025-04-28 21:21:13,457 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:13" (3/3) ...
[2025-04-28 21:21:13,458 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:13,483 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:13,487 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 26 locations, 36 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:13,548 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:13,565 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;@18600720, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:13,565 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:13,570 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 26 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 7 states have call successors, (7), 6 states have call predecessors, (7), 6 states have return successors, (7), 7 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:13,582 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:13,582 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,584 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:13,585 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,592 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,593 INFO  L85        PathProgramCache]: Analyzing trace with hash -392045088, now seen corresponding path program 1 times
[2025-04-28 21:21:13,603 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,604 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1602949488]
[2025-04-28 21:21:13,605 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,606 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,650 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:13,668 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:13,669 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,669 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:13,827 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:13,828 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:13,828 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1602949488]
[2025-04-28 21:21:13,829 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1602949488] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:13,829 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:13,833 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:13,836 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [28307958]
[2025-04-28 21:21:13,839 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:13,845 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:13,845 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:13,881 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:13,881 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:13,883 INFO  L87              Difference]: Start difference. First operand  has 26 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 7 states have call successors, (7), 6 states have call predecessors, (7), 6 states have return successors, (7), 7 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:13,934 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:13,934 INFO  L93              Difference]: Finished difference Result 26 states and 29 transitions.
[2025-04-28 21:21:13,936 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:13,937 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:13,938 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:13,945 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:13,945 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:13,948 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:13,953 INFO  L437           NwaCegarLoop]: 26 mSDtfsCounter, 1 mSDsluCounter, 42 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 68 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:13,958 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 68 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:13,973 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:14,014 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:14,017 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 13 states have internal predecessors, (14), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (8), 7 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:14,021 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:14,023 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 15
[2025-04-28 21:21:14,023 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,024 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:14,024 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:14,024 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:14,025 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:14,025 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,025 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,026 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:14,026 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,027 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,027 INFO  L85        PathProgramCache]: Analyzing trace with hash 1226648164, now seen corresponding path program 1 times
[2025-04-28 21:21:14,027 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,027 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1691635508]
[2025-04-28 21:21:14,027 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,027 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:14,045 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:14,048 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,048 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,156 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:14,157 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,157 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1691635508]
[2025-04-28 21:21:14,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1691635508] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,157 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:14,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1202156894]
[2025-04-28 21:21:14,158 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,160 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:14,160 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,161 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:14,162 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:14,162 INFO  L87              Difference]: Start difference. First operand 26 states and 29 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:14,209 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,209 INFO  L93              Difference]: Finished difference Result 30 states and 33 transitions.
[2025-04-28 21:21:14,210 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:14,210 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:14,211 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,211 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:14,211 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:14,212 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:14,213 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 1 mSDsluCounter, 45 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 73 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,213 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 73 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:14,214 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:14,218 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 26.
[2025-04-28 21:21:14,218 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 12 states have internal predecessors, (14), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (8), 7 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:14,219 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:14,219 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 15
[2025-04-28 21:21:14,220 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,220 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:14,220 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:14,220 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:14,221 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:21:14,221 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,221 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,221 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:14,221 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,222 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,222 INFO  L85        PathProgramCache]: Analyzing trace with hash 1513047071, now seen corresponding path program 1 times
[2025-04-28 21:21:14,222 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,222 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1870535560]
[2025-04-28 21:21:14,222 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,223 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,236 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:14,263 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:14,266 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,266 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,366 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:14,366 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,366 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1870535560]
[2025-04-28 21:21:14,366 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1870535560] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,366 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,366 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:14,367 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1264034957]
[2025-04-28 21:21:14,367 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,367 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:14,367 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,368 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:14,369 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:14,369 INFO  L87              Difference]: Start difference. First operand 26 states and 29 transitions. Second operand  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 2 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 2 states have call successors, (7)
[2025-04-28 21:21:14,392 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,393 INFO  L93              Difference]: Finished difference Result 28 states and 30 transitions.
[2025-04-28 21:21:14,393 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:14,393 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 2 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 2 states have call successors, (7) Word has length 26
[2025-04-28 21:21:14,394 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,394 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:14,395 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:14,395 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:14,396 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 44 mSDsCounter, 0 mSdLazyCounter, 4 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 71 SdHoareTripleChecker+Invalid, 5 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 4 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,396 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 71 Invalid, 5 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 4 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:14,397 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:14,400 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:14,401 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (8), 7 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:14,402 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:14,402 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 26
[2025-04-28 21:21:14,403 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,403 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:14,406 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 2 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 2 states have call successors, (7)
[2025-04-28 21:21:14,406 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:14,406 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:21:14,406 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,407 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,407 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:14,407 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,408 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,408 INFO  L85        PathProgramCache]: Analyzing trace with hash 996716195, now seen corresponding path program 1 times
[2025-04-28 21:21:14,408 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,408 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1627153008]
[2025-04-28 21:21:14,408 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,408 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,420 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:14,440 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:14,440 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,440 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,707 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:14,708 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,708 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1627153008]
[2025-04-28 21:21:14,708 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1627153008] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:14,708 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [199875082]
[2025-04-28 21:21:14,709 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,709 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:14,712 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,717 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:14,719 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:14,778 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:14,812 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:14,812 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,813 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,817 INFO  L256         TraceCheckSpWp]: Trace formula consists of 99 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:14,825 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:15,028 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:15,029 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:16,077 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:16,078 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [199875082] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:16,078 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:16,078 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 8
[2025-04-28 21:21:16,079 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1890743538]
[2025-04-28 21:21:16,079 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,079 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:16,080 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,081 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:16,081 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:16,082 INFO  L87              Difference]: Start difference. First operand 26 states and 27 transitions. Second operand  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 6 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:16,153 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,153 INFO  L93              Difference]: Finished difference Result 30 states and 31 transitions.
[2025-04-28 21:21:16,158 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:16,158 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 6 states have call predecessors, (9), 4 states have call successors, (9) Word has length 26
[2025-04-28 21:21:16,158 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,159 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:16,159 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:16,159 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 50 SyntacticMatches, 2 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:16,160 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 2 mSDsluCounter, 121 mSDsCounter, 0 mSdLazyCounter, 27 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 145 SdHoareTripleChecker+Invalid, 27 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 27 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,160 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 145 Invalid, 27 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 27 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:16,161 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:16,167 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:16,167 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 6 states have call predecessors, (7), 9 states have return successors, (10), 9 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:16,168 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 31 transitions.
[2025-04-28 21:21:16,168 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 31 transitions. Word has length 26
[2025-04-28 21:21:16,168 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,169 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 31 transitions.
[2025-04-28 21:21:16,169 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 6 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:16,169 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 31 transitions.
[2025-04-28 21:21:16,170 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:16,170 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,170 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,176 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:16,372 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:16,373 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,373 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,373 INFO  L85        PathProgramCache]: Analyzing trace with hash -984896800, now seen corresponding path program 2 times
[2025-04-28 21:21:16,373 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,374 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [831042900]
[2025-04-28 21:21:16,374 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:16,374 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,384 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:16,406 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:16,406 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:16,406 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,790 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:16,790 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,790 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [831042900]
[2025-04-28 21:21:16,790 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [831042900] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:16,790 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1377200286]
[2025-04-28 21:21:16,790 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:16,790 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:16,793 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,795 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:16,798 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:16,869 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:16,902 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:16,902 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:16,902 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,904 INFO  L256         TraceCheckSpWp]: Trace formula consists of 151 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:16,906 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:17,037 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:17,037 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:19,444 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:19,445 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1377200286] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:19,445 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:19,445 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 15
[2025-04-28 21:21:19,446 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1600516623]
[2025-04-28 21:21:19,447 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,447 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:19,447 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,448 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:19,448 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=171, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:19,448 INFO  L87              Difference]: Start difference. First operand 30 states and 31 transitions. Second operand  has 15 states, 7 states have (on average 2.857142857142857) internal successors, (20), 15 states have internal predecessors, (20), 9 states have call successors, (17), 1 states have call predecessors, (17), 7 states have return successors, (17), 11 states have call predecessors, (17), 9 states have call successors, (17)
[2025-04-28 21:21:19,641 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,642 INFO  L93              Difference]: Finished difference Result 37 states and 38 transitions.
[2025-04-28 21:21:19,642 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:19,643 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.857142857142857) internal successors, (20), 15 states have internal predecessors, (20), 9 states have call successors, (17), 1 states have call predecessors, (17), 7 states have return successors, (17), 11 states have call predecessors, (17), 9 states have call successors, (17) Word has length 37
[2025-04-28 21:21:19,643 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,644 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:21:19,644 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:21:19,644 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 89 GetRequests, 68 SyntacticMatches, 3 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 61 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=73, Invalid=307, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:19,645 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 12 mSDsluCounter, 145 mSDsCounter, 0 mSdLazyCounter, 57 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 166 SdHoareTripleChecker+Invalid, 68 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 57 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,645 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 166 Invalid, 68 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 57 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:21:19,655 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 35.
[2025-04-28 21:21:19,655 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 16 states have (on average 1.0625) internal successors, (17), 16 states have internal predecessors, (17), 7 states have call successors, (7), 7 states have call predecessors, (7), 11 states have return successors, (12), 11 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:19,657 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 36 transitions.
[2025-04-28 21:21:19,657 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 36 transitions. Word has length 37
[2025-04-28 21:21:19,660 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,660 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 36 transitions.
[2025-04-28 21:21:19,660 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.857142857142857) internal successors, (20), 15 states have internal predecessors, (20), 9 states have call successors, (17), 1 states have call predecessors, (17), 7 states have return successors, (17), 11 states have call predecessors, (17), 9 states have call successors, (17)
[2025-04-28 21:21:19,661 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 36 transitions.
[2025-04-28 21:21:19,661 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:19,662 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,662 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,668 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:19,862 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:19,863 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,863 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,863 INFO  L85        PathProgramCache]: Analyzing trace with hash 1913034335, now seen corresponding path program 3 times
[2025-04-28 21:21:19,864 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,868 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1078620024]
[2025-04-28 21:21:19,869 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:19,869 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,881 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 4 equivalence classes.
[2025-04-28 21:21:19,908 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:19,910 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:19,910 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,700 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 4 proven. 22 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:20,700 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,700 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1078620024]
[2025-04-28 21:21:20,700 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1078620024] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:20,700 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1802121007]
[2025-04-28 21:21:20,700 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:20,701 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,703 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,705 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:20,709 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:20,797 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 4 equivalence classes.
[2025-04-28 21:21:20,833 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:20,833 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:20,833 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,835 INFO  L256         TraceCheckSpWp]: Trace formula consists of 203 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:20,837 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,198 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 2 proven. 22 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:21,199 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,946 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 2 proven. 25 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:25,946 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1802121007] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,946 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,946 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 13, 15] total 28
[2025-04-28 21:21:25,946 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [179696898]
[2025-04-28 21:21:25,946 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,947 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:25,947 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,948 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:25,948 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=665, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:25,949 INFO  L87              Difference]: Start difference. First operand 35 states and 36 transitions. Second operand  has 28 states, 15 states have (on average 2.2) internal successors, (33), 28 states have internal predecessors, (33), 14 states have call successors, (26), 1 states have call predecessors, (26), 15 states have return successors, (31), 23 states have call predecessors, (31), 14 states have call successors, (31)
[2025-04-28 21:21:26,299 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,299 INFO  L93              Difference]: Finished difference Result 39 states and 40 transitions.
[2025-04-28 21:21:26,300 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:26,301 INFO  L79                 Accepts]: Start accepts. Automaton has  has 28 states, 15 states have (on average 2.2) internal successors, (33), 28 states have internal predecessors, (33), 14 states have call successors, (26), 1 states have call predecessors, (26), 15 states have return successors, (31), 23 states have call predecessors, (31), 14 states have call successors, (31) Word has length 48
[2025-04-28 21:21:26,301 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,302 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:21:26,302 INFO  L226             Difference]: Without dead ends: 39
[2025-04-28 21:21:26,303 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 118 GetRequests, 80 SyntacticMatches, 4 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 306 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=180, Invalid=1080, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:21:26,304 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 22 mSDsluCounter, 286 mSDsCounter, 0 mSdLazyCounter, 94 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 308 SdHoareTripleChecker+Invalid, 121 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 94 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,304 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 308 Invalid, 121 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 94 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:26,305 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 39 states.
[2025-04-28 21:21:26,308 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 39 to 39.
[2025-04-28 21:21:26,309 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 39 states, 18 states have (on average 1.0555555555555556) internal successors, (19), 18 states have internal predecessors, (19), 7 states have call successors, (7), 7 states have call predecessors, (7), 13 states have return successors, (14), 13 states have call predecessors, (14), 7 states have call successors, (14)
[2025-04-28 21:21:26,310 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 40 transitions.
[2025-04-28 21:21:26,310 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 40 transitions. Word has length 48
[2025-04-28 21:21:26,310 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,310 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 40 transitions.
[2025-04-28 21:21:26,310 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 28 states, 15 states have (on average 2.2) internal successors, (33), 28 states have internal predecessors, (33), 14 states have call successors, (26), 1 states have call predecessors, (26), 15 states have return successors, (31), 23 states have call predecessors, (31), 14 states have call successors, (31)
[2025-04-28 21:21:26,310 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 40 transitions.
[2025-04-28 21:21:26,312 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:26,312 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,312 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,316 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:26,514 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,514 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,515 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,515 INFO  L85        PathProgramCache]: Analyzing trace with hash 2067760988, now seen corresponding path program 4 times
[2025-04-28 21:21:26,515 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,515 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [759445428]
[2025-04-28 21:21:26,515 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:26,515 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,527 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 59 statements into 2 equivalence classes.
[2025-04-28 21:21:26,540 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:26,540 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:26,540 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,108 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 42 refuted. 0 times theorem prover too weak. 33 trivial. 0 not checked.
[2025-04-28 21:21:27,108 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,108 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [759445428]
[2025-04-28 21:21:27,108 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [759445428] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,108 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [865946537]
[2025-04-28 21:21:27,108 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:27,109 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,112 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,114 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:27,118 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,253 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 59 statements into 2 equivalence classes.
[2025-04-28 21:21:27,298 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:27,299 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:27,299 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,301 INFO  L256         TraceCheckSpWp]: Trace formula consists of 255 conjuncts, 26 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,305 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,512 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 38 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:27,512 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,850 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 47 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:35,850 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [865946537] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,850 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,850 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 15, 19] total 27
[2025-04-28 21:21:35,850 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1764954988]
[2025-04-28 21:21:35,850 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,851 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:21:35,851 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,852 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:21:35,852 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=115, Invalid=587, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:35,853 INFO  L87              Difference]: Start difference. First operand 39 states and 40 transitions. Second operand  has 27 states, 13 states have (on average 2.4615384615384617) internal successors, (32), 27 states have internal predecessors, (32), 15 states have call successors, (27), 1 states have call predecessors, (27), 13 states have return successors, (33), 21 states have call predecessors, (33), 15 states have call successors, (33)
[2025-04-28 21:21:36,129 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,130 INFO  L93              Difference]: Finished difference Result 47 states and 48 transitions.
[2025-04-28 21:21:36,130 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:36,131 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 13 states have (on average 2.4615384615384617) internal successors, (32), 27 states have internal predecessors, (32), 15 states have call successors, (27), 1 states have call predecessors, (27), 13 states have return successors, (33), 21 states have call predecessors, (33), 15 states have call successors, (33) Word has length 59
[2025-04-28 21:21:36,132 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,134 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:36,135 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:36,136 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 144 GetRequests, 106 SyntacticMatches, 5 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 360 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=221, Invalid=969, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:36,137 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 21 mSDsluCounter, 212 mSDsCounter, 0 mSdLazyCounter, 73 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 234 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 73 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,138 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 234 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 73 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,142 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:36,150 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 47.
[2025-04-28 21:21:36,150 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 22 states have (on average 1.0454545454545454) internal successors, (23), 22 states have internal predecessors, (23), 7 states have call successors, (7), 7 states have call predecessors, (7), 17 states have return successors, (18), 17 states have call predecessors, (18), 7 states have call successors, (18)
[2025-04-28 21:21:36,151 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 48 transitions.
[2025-04-28 21:21:36,151 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 48 transitions. Word has length 59
[2025-04-28 21:21:36,151 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,151 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 48 transitions.
[2025-04-28 21:21:36,152 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 13 states have (on average 2.4615384615384617) internal successors, (32), 27 states have internal predecessors, (32), 15 states have call successors, (27), 1 states have call predecessors, (27), 13 states have return successors, (33), 21 states have call predecessors, (33), 15 states have call successors, (33)
[2025-04-28 21:21:36,152 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 48 transitions.
[2025-04-28 21:21:36,153 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 82
[2025-04-28 21:21:36,153 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,153 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,158 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:36,356 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,356 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,356 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,357 INFO  L85        PathProgramCache]: Analyzing trace with hash 798670808, now seen corresponding path program 5 times
[2025-04-28 21:21:36,357 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,357 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [721042765]
[2025-04-28 21:21:36,357 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:36,357 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,379 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 81 statements into 7 equivalence classes.
[2025-04-28 21:21:36,419 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 81 of 81 statements.
[2025-04-28 21:21:36,421 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:36,421 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,261 INFO  L134       CoverageAnalysis]: Checked inductivity of 183 backedges. 5 proven. 90 refuted. 0 times theorem prover too weak. 88 trivial. 0 not checked.
[2025-04-28 21:21:37,262 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,262 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [721042765]
[2025-04-28 21:21:37,262 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [721042765] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,262 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [847702861]
[2025-04-28 21:21:37,262 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:37,262 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,265 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,269 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:37,273 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,508 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 81 statements into 7 equivalence classes.
[2025-04-28 21:21:37,571 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 81 of 81 statements.
[2025-04-28 21:21:37,571 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:37,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,574 INFO  L256         TraceCheckSpWp]: Trace formula consists of 359 conjuncts, 36 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,577 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,760 INFO  L134       CoverageAnalysis]: Checked inductivity of 183 backedges. 5 proven. 82 refuted. 0 times theorem prover too weak. 96 trivial. 0 not checked.
[2025-04-28 21:21:37,760 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
