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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:31,971 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:32,088 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e0d6e149-30cb-46fb-85aa-9fd52f713956/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:32,094 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:32,095 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:32,119 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:32,119 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:32,120 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:32,120 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:32,120 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:32,121 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:32,121 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:32,121 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:32,121 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:32,121 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:32,121 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:32,122 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:32,122 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:32,122 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:32,122 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:32,122 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:32,122 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:32,123 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:32,123 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:32,123 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:32,124 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:32,124 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:32,511 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:32,525 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:32,529 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:32,532 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:32,532 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:32,533 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e0d6e149-30cb-46fb-85aa-9fd52f713956/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-026.smt2
[2025-04-28 21:21:32,536 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:32,540 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:32,804 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e0d6e149-30cb-46fb-85aa-9fd52f713956/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-026.smt2
[2025-04-28 21:21:32,808 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:32,810 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:32,811 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:32,811 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:32,811 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:32,816 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,851 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32 Unit
[2025-04-28 21:21:32,853 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:32,856 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:32,856 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:32,857 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:32,875 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,876 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,915 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,916 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,919 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,921 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,927 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,928 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,931 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,952 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:32,954 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:32,954 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:32,954 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:32,955 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,958 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:32,977 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,998 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:33,004 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:33,019 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:33,020 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:33,021 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:33,021 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:33,022 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:33,022 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:33,022 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure sum given in one single declaration
[2025-04-28 21:21:33,022 INFO  L130     BoogieDeclarations]: Found specification of procedure sum
[2025-04-28 21:21:33,022 INFO  L138     BoogieDeclarations]: Found implementation of procedure sum
[2025-04-28 21:21:33,022 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure sum.AT.split given in one single declaration
[2025-04-28 21:21:33,022 INFO  L130     BoogieDeclarations]: Found specification of procedure sum.AT.split
[2025-04-28 21:21:33,022 INFO  L138     BoogieDeclarations]: Found implementation of procedure sum.AT.split
[2025-04-28 21:21:33,022 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure sum.AT_call given in one single declaration
[2025-04-28 21:21:33,023 INFO  L130     BoogieDeclarations]: Found specification of procedure sum.AT_call
[2025-04-28 21:21:33,023 INFO  L138     BoogieDeclarations]: Found implementation of procedure sum.AT_call
[2025-04-28 21:21:33,024 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:33,024 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:33,025 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:33,025 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:33,025 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:33,025 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:33,090 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:33,092 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:33,215 INFO  L?                        ?]: Removed 15 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:33,215 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:33,238 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:33,238 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:33,239 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:33 BoogieIcfgContainer
[2025-04-28 21:21:33,242 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:33,245 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:33,246 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:33,254 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:33,254 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:32" (1/3) ...
[2025-04-28 21:21:33,255 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@312ed14f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:33, skipping insertion in model container
[2025-04-28 21:21:33,255 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (2/3) ...
[2025-04-28 21:21:33,256 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@312ed14f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:33, skipping insertion in model container
[2025-04-28 21:21:33,256 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:33" (3/3) ...
[2025-04-28 21:21:33,258 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:33,278 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:33,281 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:33,345 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:33,374 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;@962cf9b, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:33,374 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:33,384 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:33,395 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:33,396 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,397 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:33,398 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,405 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,405 INFO  L85        PathProgramCache]: Analyzing trace with hash -392045088, now seen corresponding path program 1 times
[2025-04-28 21:21:33,415 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,415 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1367509717]
[2025-04-28 21:21:33,415 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,416 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,453 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:33,476 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:33,477 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,477 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,617 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:33,617 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,618 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1367509717]
[2025-04-28 21:21:33,619 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1367509717] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,619 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,623 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:33,628 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1816022840]
[2025-04-28 21:21:33,629 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,633 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:33,634 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,672 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:33,673 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:33,677 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:33,730 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,731 INFO  L93              Difference]: Finished difference Result 26 states and 29 transitions.
[2025-04-28 21:21:33,732 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:33,734 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:33,735 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,743 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:33,743 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:33,747 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:33,755 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:33,756 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:33,775 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:33,804 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:33,806 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:33,818 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:33,819 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 15
[2025-04-28 21:21:33,820 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,820 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:33,821 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:33,821 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:33,825 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:33,826 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,826 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:33,826 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:33,826 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,828 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,828 INFO  L85        PathProgramCache]: Analyzing trace with hash 1226648164, now seen corresponding path program 1 times
[2025-04-28 21:21:33,829 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,829 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1081180407]
[2025-04-28 21:21:33,829 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,829 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,838 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:33,852 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:33,852 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,852 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,911 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:33,911 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1081180407]
[2025-04-28 21:21:33,911 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1081180407] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,912 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,912 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:33,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1228720223]
[2025-04-28 21:21:33,912 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,913 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:33,914 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,914 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:33,914 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:33,915 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:33,943 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,943 INFO  L93              Difference]: Finished difference Result 30 states and 33 transitions.
[2025-04-28 21:21:33,947 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:33,947 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:33,947 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,948 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:33,970 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:33,970 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:33,971 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:33,972 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:33,973 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:33,980 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 26.
[2025-04-28 21:21:33,980 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:33,982 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 29 transitions.
[2025-04-28 21:21:33,983 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 29 transitions. Word has length 15
[2025-04-28 21:21:33,983 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,983 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 29 transitions.
[2025-04-28 21:21:33,983 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:33,983 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 29 transitions.
[2025-04-28 21:21:33,984 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:21:33,984 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,984 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:33,985 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:33,985 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,986 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,986 INFO  L85        PathProgramCache]: Analyzing trace with hash 1513047071, now seen corresponding path program 1 times
[2025-04-28 21:21:33,987 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,987 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [36031881]
[2025-04-28 21:21:33,987 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,987 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,008 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:34,036 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:34,037 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,037 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,156 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:34,157 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,157 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [36031881]
[2025-04-28 21:21:34,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [36031881] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,157 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:34,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1304968851]
[2025-04-28 21:21:34,157 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:34,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:34,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:34,159 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:34,180 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,180 INFO  L93              Difference]: Finished difference Result 28 states and 30 transitions.
[2025-04-28 21:21:34,181 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:34,181 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:34,182 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,182 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:34,182 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:34,183 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:34,184 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:34,185 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:34,186 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:34,192 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:34,195 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:34,196 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:34,197 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 26
[2025-04-28 21:21:34,197 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,197 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:34,197 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:34,197 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:34,198 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-04-28 21:21:34,198 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,198 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:34,198 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:34,198 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,200 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,200 INFO  L85        PathProgramCache]: Analyzing trace with hash 996716195, now seen corresponding path program 1 times
[2025-04-28 21:21:34,200 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,204 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [762611201]
[2025-04-28 21:21:34,204 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,205 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,220 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:34,241 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:34,243 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,243 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,615 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:34,615 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,615 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [762611201]
[2025-04-28 21:21:34,615 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [762611201] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,615 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1782274038]
[2025-04-28 21:21:34,616 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,616 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,619 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,623 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:34,626 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,699 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-04-28 21:21:34,732 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-04-28 21:21:34,732 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,736 INFO  L256         TraceCheckSpWp]: Trace formula consists of 99 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,744 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,955 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:34,955 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,933 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:35,934 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1782274038] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,934 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,934 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 8
[2025-04-28 21:21:35,935 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1457871466]
[2025-04-28 21:21:35,935 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,935 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:35,935 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,936 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:35,938 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:35,938 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:36,004 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,008 INFO  L93              Difference]: Finished difference Result 30 states and 31 transitions.
[2025-04-28 21:21:36,009 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:36,009 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:36,009 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,010 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:36,014 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:36,014 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:36,015 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:36,016 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:36,017 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:36,022 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:36,022 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:36,024 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 31 transitions.
[2025-04-28 21:21:36,025 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 31 transitions. Word has length 26
[2025-04-28 21:21:36,026 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,026 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 31 transitions.
[2025-04-28 21:21:36,026 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:36,026 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 31 transitions.
[2025-04-28 21:21:36,027 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:36,028 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,028 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:36,034 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:36,232 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:36,233 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,233 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,233 INFO  L85        PathProgramCache]: Analyzing trace with hash -984896800, now seen corresponding path program 2 times
[2025-04-28 21:21:36,233 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,233 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1419807965]
[2025-04-28 21:21:36,234 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:36,234 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,244 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:36,261 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:36,261 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:36,261 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,619 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:36,619 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,619 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1419807965]
[2025-04-28 21:21:36,619 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1419807965] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,619 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [634439875]
[2025-04-28 21:21:36,619 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:36,619 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,622 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,625 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:36,630 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,691 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:36,724 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:36,724 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:36,724 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,726 INFO  L256         TraceCheckSpWp]: Trace formula consists of 151 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,728 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,854 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:36,854 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,397 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:39,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [634439875] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,397 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,398 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 15
[2025-04-28 21:21:39,398 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1856978213]
[2025-04-28 21:21:39,398 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,398 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:39,398 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,399 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:39,400 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=171, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:39,401 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:39,579 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,579 INFO  L93              Difference]: Finished difference Result 37 states and 38 transitions.
[2025-04-28 21:21:39,579 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:39,580 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:39,580 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,581 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:21:39,581 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:21:39,581 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:39,582 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:39,583 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:39,584 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:21:39,587 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 35.
[2025-04-28 21:21:39,588 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:39,589 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 36 transitions.
[2025-04-28 21:21:39,589 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 36 transitions. Word has length 37
[2025-04-28 21:21:39,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,589 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 36 transitions.
[2025-04-28 21:21:39,589 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:39,590 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 36 transitions.
[2025-04-28 21:21:39,591 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:39,591 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,591 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:39,598 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:39,795 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:39,796 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,796 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,796 INFO  L85        PathProgramCache]: Analyzing trace with hash 1913034335, now seen corresponding path program 3 times
[2025-04-28 21:21:39,796 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,797 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [173394512]
[2025-04-28 21:21:39,797 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,797 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,809 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 4 equivalence classes.
[2025-04-28 21:21:39,848 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:39,848 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:39,848 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,486 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:40,486 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,486 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [173394512]
[2025-04-28 21:21:40,486 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [173394512] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,486 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1584865314]
[2025-04-28 21:21:40,486 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:40,486 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,489 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,491 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:40,499 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,578 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 4 equivalence classes.
[2025-04-28 21:21:40,617 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:40,617 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:40,617 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,619 INFO  L256         TraceCheckSpWp]: Trace formula consists of 203 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,625 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,942 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:40,942 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,819 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:45,819 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1584865314] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,820 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,820 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 13, 15] total 28
[2025-04-28 21:21:45,820 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [957601492]
[2025-04-28 21:21:45,820 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,820 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:45,821 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,822 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:45,822 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=665, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:45,823 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:46,182 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,183 INFO  L93              Difference]: Finished difference Result 39 states and 40 transitions.
[2025-04-28 21:21:46,183 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:46,183 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:46,184 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,184 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:21:46,185 INFO  L226             Difference]: Without dead ends: 39
[2025-04-28 21:21:46,185 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:46,186 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:46,187 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:46,187 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 39 states.
[2025-04-28 21:21:46,191 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 39 to 39.
[2025-04-28 21:21:46,191 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:46,192 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 40 transitions.
[2025-04-28 21:21:46,192 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 40 transitions. Word has length 48
[2025-04-28 21:21:46,193 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,193 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 40 transitions.
[2025-04-28 21:21:46,193 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:46,193 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 40 transitions.
[2025-04-28 21:21:46,194 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:46,194 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,195 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:46,200 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,397 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:46,397 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,397 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,397 INFO  L85        PathProgramCache]: Analyzing trace with hash 2067760988, now seen corresponding path program 4 times
[2025-04-28 21:21:46,397 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,398 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1099525203]
[2025-04-28 21:21:46,398 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:46,398 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,408 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 59 statements into 2 equivalence classes.
[2025-04-28 21:21:46,420 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:46,420 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:46,420 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,897 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:46,897 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,897 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1099525203]
[2025-04-28 21:21:46,897 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1099525203] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,898 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [498848531]
[2025-04-28 21:21:46,898 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:46,898 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,901 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,903 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:46,907 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,065 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 59 statements into 2 equivalence classes.
[2025-04-28 21:21:47,110 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:47,110 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:47,110 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,112 INFO  L256         TraceCheckSpWp]: Trace formula consists of 255 conjuncts, 26 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,115 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,272 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:47,272 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,805 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:55,805 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [498848531] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:55,805 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:55,806 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 15, 19] total 23
[2025-04-28 21:21:55,806 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [577494803]
[2025-04-28 21:21:55,806 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,806 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:55,807 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,807 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:55,808 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=415, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:55,808 INFO  L87              Difference]: Start difference. First operand 39 states and 40 transitions. Second operand  has 23 states, 11 states have (on average 2.5454545454545454) internal successors, (28), 23 states have internal predecessors, (28), 13 states have call successors, (23), 1 states have call predecessors, (23), 11 states have return successors, (29), 17 states have call predecessors, (29), 13 states have call successors, (29)
[2025-04-28 21:21:56,020 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,020 INFO  L93              Difference]: Finished difference Result 43 states and 44 transitions.
[2025-04-28 21:21:56,022 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:56,022 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 2.5454545454545454) internal successors, (28), 23 states have internal predecessors, (28), 13 states have call successors, (23), 1 states have call predecessors, (23), 11 states have return successors, (29), 17 states have call predecessors, (29), 13 states have call successors, (29) Word has length 59
[2025-04-28 21:21:56,023 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,023 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:56,023 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:56,024 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 142 GetRequests, 110 SyntacticMatches, 5 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 218 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=161, Invalid=651, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:56,025 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 12 mSDsluCounter, 263 mSDsCounter, 0 mSdLazyCounter, 83 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 285 SdHoareTripleChecker+Invalid, 96 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 83 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,025 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 285 Invalid, 96 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 83 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,026 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:56,030 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 43.
[2025-04-28 21:21:56,030 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 43 states, 20 states have (on average 1.05) internal successors, (21), 20 states have internal predecessors, (21), 7 states have call successors, (7), 7 states have call predecessors, (7), 15 states have return successors, (16), 15 states have call predecessors, (16), 7 states have call successors, (16)
[2025-04-28 21:21:56,031 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 43 states to 43 states and 44 transitions.
[2025-04-28 21:21:56,031 INFO  L79                 Accepts]: Start accepts. Automaton has 43 states and 44 transitions. Word has length 59
[2025-04-28 21:21:56,031 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,032 INFO  L485      AbstractCegarLoop]: Abstraction has 43 states and 44 transitions.
[2025-04-28 21:21:56,032 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 2.5454545454545454) internal successors, (28), 23 states have internal predecessors, (28), 13 states have call successors, (23), 1 states have call predecessors, (23), 11 states have return successors, (29), 17 states have call predecessors, (29), 13 states have call successors, (29)
[2025-04-28 21:21:56,032 INFO  L278                IsEmpty]: Start isEmpty. Operand 43 states and 44 transitions.
[2025-04-28 21:21:56,033 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 71
[2025-04-28 21:21:56,033 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,033 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,039 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:56,236 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:56,236 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,237 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,237 INFO  L85        PathProgramCache]: Analyzing trace with hash 1069574683, now seen corresponding path program 5 times
[2025-04-28 21:21:56,237 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,237 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [36722680]
[2025-04-28 21:21:56,237 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,237 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,254 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 70 statements into 6 equivalence classes.
[2025-04-28 21:21:56,273 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 70 of 70 statements.
[2025-04-28 21:21:56,273 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:56,273 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,951 INFO  L134       CoverageAnalysis]: Checked inductivity of 125 backedges. 4 proven. 64 refuted. 0 times theorem prover too weak. 57 trivial. 0 not checked.
[2025-04-28 21:21:56,951 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,952 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [36722680]
[2025-04-28 21:21:56,952 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [36722680] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,952 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [101895321]
[2025-04-28 21:21:56,952 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,952 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,955 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,957 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:56,961 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,196 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 70 statements into 6 equivalence classes.
[2025-04-28 21:21:57,246 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 70 of 70 statements.
[2025-04-28 21:21:57,246 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:57,246 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,248 INFO  L256         TraceCheckSpWp]: Trace formula consists of 307 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,251 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,411 INFO  L134       CoverageAnalysis]: Checked inductivity of 125 backedges. 4 proven. 58 refuted. 0 times theorem prover too weak. 63 trivial. 0 not checked.
[2025-04-28 21:21:57,411 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
