./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-128.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:11,426 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:11,543 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_99541def-c1e9-45f0-8160-5f0f041a0a53/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:11,553 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:11,557 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:11,592 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:11,592 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:11,593 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:11,593 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:11,593 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:11,593 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:11,594 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:11,594 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:11,594 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:11,594 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:11,594 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:11,594 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:11,594 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:11,595 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:11,595 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:11,595 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:11,595 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:11,595 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:11,595 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:11,595 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:11,596 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:11,596 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:11,966 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:11,978 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:11,981 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:11,984 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:11,985 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:11,986 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_99541def-c1e9-45f0-8160-5f0f041a0a53/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-128.smt2
[2025-04-28 21:21:11,987 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:11,991 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:12,208 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_99541def-c1e9-45f0-8160-5f0f041a0a53/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-128.smt2
[2025-04-28 21:21:12,211 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:12,213 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:12,214 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:12,214 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:12,214 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:12,217 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,255 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12 Unit
[2025-04-28 21:21:12,257 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:12,258 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,259 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:12,259 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:12,276 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,276 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,303 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,303 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,306 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,307 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,309 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,310 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,311 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,325 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:12,331 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:12,332 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:12,332 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:12,333 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (1/1) ...
[2025-04-28 21:21:12,336 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:12,351 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:12,368 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:12,375 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:12,390 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:12,390 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:12,390 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:12,390 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure init.DLRunknown.CLN6 given in one single declaration
[2025-04-28 21:21:12,391 INFO  L130     BoogieDeclarations]: Found specification of procedure init.DLRunknown.CLN6
[2025-04-28 21:21:12,391 INFO  L138     BoogieDeclarations]: Found implementation of procedure init.DLRunknown.CLN6
[2025-04-28 21:21:12,391 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure init.DLRunknown.CLN4 given in one single declaration
[2025-04-28 21:21:12,391 INFO  L130     BoogieDeclarations]: Found specification of procedure init.DLRunknown.CLN4
[2025-04-28 21:21:12,392 INFO  L138     BoogieDeclarations]: Found implementation of procedure init.DLRunknown.CLN4
[2025-04-28 21:21:12,392 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN15 given in one single declaration
[2025-04-28 21:21:12,392 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN15
[2025-04-28 21:21:12,392 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN15
[2025-04-28 21:21:12,392 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure update.DLRunknown.CLN12 given in one single declaration
[2025-04-28 21:21:12,393 INFO  L130     BoogieDeclarations]: Found specification of procedure update.DLRunknown.CLN12
[2025-04-28 21:21:12,393 INFO  L138     BoogieDeclarations]: Found implementation of procedure update.DLRunknown.CLN12
[2025-04-28 21:21:12,394 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure mk_array.DLRunknown.CLN9 given in one single declaration
[2025-04-28 21:21:12,394 INFO  L130     BoogieDeclarations]: Found specification of procedure mk_array.DLRunknown.CLN9
[2025-04-28 21:21:12,394 INFO  L138     BoogieDeclarations]: Found implementation of procedure mk_array.DLRunknown.CLN9
[2025-04-28 21:21:12,394 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:12,394 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:12,394 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:12,448 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:12,451 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:12,627 INFO  L?                        ?]: Removed 18 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:12,628 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:12,639 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:12,640 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:12,640 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12 BoogieIcfgContainer
[2025-04-28 21:21:12,641 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:12,644 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:12,645 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:12,649 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:12,649 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:12" (1/3) ...
[2025-04-28 21:21:12,650 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2b078bc and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,650 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:12" (2/3) ...
[2025-04-28 21:21:12,651 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2b078bc and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:12, skipping insertion in model container
[2025-04-28 21:21:12,651 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:12" (3/3) ...
[2025-04-28 21:21:12,652 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:12,672 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:12,675 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 30 locations, 43 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:12,732 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:12,749 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;@65374b30, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:12,749 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:12,754 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 30 states, 14 states have (on average 1.3571428571428572) internal successors, (19), 18 states have internal predecessors, (19), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 8 states have call successors, (8)
[2025-04-28 21:21:12,762 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:12,762 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:12,763 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:12,763 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:12,769 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:12,770 INFO  L85        PathProgramCache]: Analyzing trace with hash 1966259693, now seen corresponding path program 1 times
[2025-04-28 21:21:12,779 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:12,780 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [570017641]
[2025-04-28 21:21:12,781 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:12,782 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:12,819 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:12,851 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:12,851 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:12,851 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:13,151 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,152 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:13,152 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [570017641]
[2025-04-28 21:21:13,153 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [570017641] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:13,153 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:13,156 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:13,158 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [386488750]
[2025-04-28 21:21:13,159 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:13,163 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:13,163 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:13,192 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:13,193 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:13,198 INFO  L87              Difference]: Start difference. First operand  has 30 states, 14 states have (on average 1.3571428571428572) internal successors, (19), 18 states have internal predecessors, (19), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 8 states have call successors, (8) Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:13,278 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:13,278 INFO  L93              Difference]: Finished difference Result 30 states and 35 transitions.
[2025-04-28 21:21:13,282 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:13,284 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:13,284 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:13,293 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:13,293 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:13,295 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,299 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 1 mSDsluCounter, 56 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 88 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:13,300 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 88 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:13,318 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:13,339 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:13,344 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 14 states have (on average 1.2857142857142858) internal successors, (18), 17 states have internal predecessors, (18), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (9), 7 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:13,349 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 35 transitions.
[2025-04-28 21:21:13,352 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 35 transitions. Word has length 17
[2025-04-28 21:21:13,353 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:13,353 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 35 transitions.
[2025-04-28 21:21:13,354 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:13,354 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 35 transitions.
[2025-04-28 21:21:13,356 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:13,358 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,359 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]
[2025-04-28 21:21:13,359 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:13,359 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,360 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,360 INFO  L85        PathProgramCache]: Analyzing trace with hash -1239195790, now seen corresponding path program 1 times
[2025-04-28 21:21:13,361 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,361 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1684196226]
[2025-04-28 21:21:13,362 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,362 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,382 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:13,440 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:13,444 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,444 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:13,732 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:13,732 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:13,733 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1684196226]
[2025-04-28 21:21:13,733 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1684196226] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:13,733 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:13,733 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:13,733 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [522424442]
[2025-04-28 21:21:13,733 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:13,734 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:13,736 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:13,737 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:13,737 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:13,737 INFO  L87              Difference]: Start difference. First operand 30 states and 35 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:13,888 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:13,889 INFO  L93              Difference]: Finished difference Result 40 states and 47 transitions.
[2025-04-28 21:21:13,890 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:13,890 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-04-28 21:21:13,891 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:13,892 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:13,893 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:13,894 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:13,898 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 3 mSDsluCounter, 143 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 173 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:13,898 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 173 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:13,899 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:13,910 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 34.
[2025-04-28 21:21:13,911 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.25) internal successors, (20), 19 states have internal predecessors, (20), 8 states have call successors, (8), 6 states have call predecessors, (8), 9 states have return successors, (11), 8 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:13,913 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 39 transitions.
[2025-04-28 21:21:13,914 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 39 transitions. Word has length 21
[2025-04-28 21:21:13,914 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:13,915 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 39 transitions.
[2025-04-28 21:21:13,915 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:13,915 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 39 transitions.
[2025-04-28 21:21:13,916 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:13,916 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:13,916 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]
[2025-04-28 21:21:13,917 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:13,917 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:13,918 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:13,918 INFO  L85        PathProgramCache]: Analyzing trace with hash 1424647473, now seen corresponding path program 1 times
[2025-04-28 21:21:13,918 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:13,918 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1186368705]
[2025-04-28 21:21:13,918 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:13,918 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:13,936 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:13,955 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:13,959 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:13,959 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,139 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,139 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,139 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1186368705]
[2025-04-28 21:21:14,139 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1186368705] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,139 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,139 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:14,139 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [655482636]
[2025-04-28 21:21:14,139 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,140 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:14,140 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,145 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:14,145 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=12, Invalid=30, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:14,145 INFO  L87              Difference]: Start difference. First operand 34 states and 39 transitions. Second operand  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:14,270 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,270 INFO  L93              Difference]: Finished difference Result 40 states and 46 transitions.
[2025-04-28 21:21:14,272 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:14,272 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5) Word has length 21
[2025-04-28 21:21:14,273 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,273 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:14,273 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:14,274 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:14,277 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 3 mSDsluCounter, 111 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 143 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:14,278 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 143 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:14,279 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:14,286 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 34.
[2025-04-28 21:21:14,289 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.25) internal successors, (20), 19 states have internal predecessors, (20), 8 states have call successors, (8), 6 states have call predecessors, (8), 9 states have return successors, (11), 8 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:14,291 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 39 transitions.
[2025-04-28 21:21:14,291 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 39 transitions. Word has length 21
[2025-04-28 21:21:14,291 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:14,292 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 39 transitions.
[2025-04-28 21:21:14,292 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:14,292 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 39 transitions.
[2025-04-28 21:21:14,293 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:14,294 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,295 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,295 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:14,295 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,296 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,298 INFO  L85        PathProgramCache]: Analyzing trace with hash -1157313413, now seen corresponding path program 1 times
[2025-04-28 21:21:14,298 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,298 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1749485936]
[2025-04-28 21:21:14,298 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,298 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,314 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:14,347 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:14,351 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,351 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,893 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:14,894 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,894 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1749485936]
[2025-04-28 21:21:14,894 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1749485936] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:14,894 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1714423906]
[2025-04-28 21:21:14,894 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,894 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:14,897 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,900 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,903 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,967 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:15,016 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:15,016 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,016 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,019 INFO  L256         TraceCheckSpWp]: Trace formula consists of 142 conjuncts, 36 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:15,029 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:15,711 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:15,712 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:21,750 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:21,751 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1714423906] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:21,751 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:21,751 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 12, 12] total 22
[2025-04-28 21:21:21,751 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1976666363]
[2025-04-28 21:21:21,751 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,753 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:21,753 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,754 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:21,756 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=409, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:21,757 INFO  L87              Difference]: Start difference. First operand 34 states and 39 transitions. Second operand  has 22 states, 12 states have (on average 2.6666666666666665) internal successors, (32), 22 states have internal predecessors, (32), 12 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (18), 11 states have call predecessors, (18), 12 states have call successors, (18)
[2025-04-28 21:21:22,342 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,342 INFO  L93              Difference]: Finished difference Result 54 states and 60 transitions.
[2025-04-28 21:21:22,342 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-04-28 21:21:22,343 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 12 states have (on average 2.6666666666666665) internal successors, (32), 22 states have internal predecessors, (32), 12 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (18), 11 states have call predecessors, (18), 12 states have call successors, (18) Word has length 33
[2025-04-28 21:21:22,343 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,344 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:22,344 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:22,345 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 88 GetRequests, 57 SyntacticMatches, 0 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 75 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=117, Invalid=939, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:22,346 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 8 mSDsluCounter, 488 mSDsCounter, 0 mSdLazyCounter, 296 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 524 SdHoareTripleChecker+Invalid, 300 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 296 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,346 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 524 Invalid, 300 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 296 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:22,347 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:22,352 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 42.
[2025-04-28 21:21:22,352 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 20 states have (on average 1.2) internal successors, (24), 24 states have internal predecessors, (24), 8 states have call successors, (8), 6 states have call predecessors, (8), 13 states have return successors, (15), 12 states have call predecessors, (15), 8 states have call successors, (15)
[2025-04-28 21:21:22,353 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 47 transitions.
[2025-04-28 21:21:22,353 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 47 transitions. Word has length 33
[2025-04-28 21:21:22,354 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,354 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 47 transitions.
[2025-04-28 21:21:22,354 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 12 states have (on average 2.6666666666666665) internal successors, (32), 22 states have internal predecessors, (32), 12 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (18), 11 states have call predecessors, (18), 12 states have call successors, (18)
[2025-04-28 21:21:22,354 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 47 transitions.
[2025-04-28 21:21:22,355 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:22,355 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,355 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,362 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:22,560 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:22,560 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,561 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,561 INFO  L85        PathProgramCache]: Analyzing trace with hash 1318702398, now seen corresponding path program 1 times
[2025-04-28 21:21:22,561 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,561 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [201175059]
[2025-04-28 21:21:22,561 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,561 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,569 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:22,580 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:22,580 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,580 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,857 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:22,857 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,857 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [201175059]
[2025-04-28 21:21:22,857 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [201175059] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,857 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1094371613]
[2025-04-28 21:21:22,857 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,857 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,861 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,863 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:22,869 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,935 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:22,963 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:22,963 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,963 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,964 INFO  L256         TraceCheckSpWp]: Trace formula consists of 161 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,966 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,028 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:23,028 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:24,463 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:24,464 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1094371613] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:24,464 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:24,464 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 13] total 15
[2025-04-28 21:21:24,464 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1511103107]
[2025-04-28 21:21:24,464 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,465 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:24,465 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,465 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:24,466 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=171, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:24,466 INFO  L87              Difference]: Start difference. First operand 42 states and 47 transitions. Second operand  has 15 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 15 states have internal predecessors, (21), 8 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 8 states have call predecessors, (12), 8 states have call successors, (12)
[2025-04-28 21:21:24,640 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,640 INFO  L93              Difference]: Finished difference Result 60 states and 66 transitions.
[2025-04-28 21:21:24,641 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:24,641 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 15 states have internal predecessors, (21), 8 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 8 states have call predecessors, (12), 8 states have call successors, (12) Word has length 37
[2025-04-28 21:21:24,641 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,642 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:24,642 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:21:24,643 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 89 GetRequests, 65 SyntacticMatches, 8 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 42 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=60, Invalid=246, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:24,643 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 6 mSDsluCounter, 253 mSDsCounter, 0 mSdLazyCounter, 125 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 291 SdHoareTripleChecker+Invalid, 128 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 125 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,644 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 291 Invalid, 128 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 125 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:24,644 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:21:24,649 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 40.
[2025-04-28 21:21:24,649 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 19 states have (on average 1.2105263157894737) internal successors, (23), 22 states have internal predecessors, (23), 8 states have call successors, (8), 6 states have call predecessors, (8), 12 states have return successors, (14), 12 states have call predecessors, (14), 8 states have call successors, (14)
[2025-04-28 21:21:24,650 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 45 transitions.
[2025-04-28 21:21:24,650 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 45 transitions. Word has length 37
[2025-04-28 21:21:24,651 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,651 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 45 transitions.
[2025-04-28 21:21:24,651 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 15 states have internal predecessors, (21), 8 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 8 states have call predecessors, (12), 8 states have call successors, (12)
[2025-04-28 21:21:24,651 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 45 transitions.
[2025-04-28 21:21:24,652 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:24,652 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,652 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,657 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:24,854 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:24,854 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,855 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,855 INFO  L85        PathProgramCache]: Analyzing trace with hash -1571468863, now seen corresponding path program 1 times
[2025-04-28 21:21:24,855 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,855 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [287024402]
[2025-04-28 21:21:24,855 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,855 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,861 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:24,872 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:24,872 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,872 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,062 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 2 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:25,062 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,062 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [287024402]
[2025-04-28 21:21:25,062 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [287024402] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:25,062 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1101263423]
[2025-04-28 21:21:25,062 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,062 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,066 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,069 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:25,074 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:25,181 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:25,211 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:25,211 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,211 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,213 INFO  L256         TraceCheckSpWp]: Trace formula consists of 166 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:25,214 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:25,264 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 1 proven. 2 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:25,264 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,861 INFO  L134       CoverageAnalysis]: Checked inductivity of 17 backedges. 3 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:27,861 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1101263423] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,862 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:27,862 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [10, 10] total 13
[2025-04-28 21:21:27,862 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1959834751]
[2025-04-28 21:21:27,862 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,862 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:27,862 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,864 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:27,864 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=127, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:27,864 INFO  L87              Difference]: Start difference. First operand 40 states and 45 transitions. Second operand  has 10 states, 7 states have (on average 2.142857142857143) internal successors, (15), 10 states have internal predecessors, (15), 4 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:27,950 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,950 INFO  L93              Difference]: Finished difference Result 56 states and 62 transitions.
[2025-04-28 21:21:27,951 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:27,951 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 7 states have (on average 2.142857142857143) internal successors, (15), 10 states have internal predecessors, (15), 4 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 37
[2025-04-28 21:21:27,951 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,952 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:27,952 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:27,952 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 86 GetRequests, 67 SyntacticMatches, 8 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=29, Invalid=127, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:27,953 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 3 mSDsluCounter, 187 mSDsCounter, 0 mSdLazyCounter, 57 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 216 SdHoareTripleChecker+Invalid, 57 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 57 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,953 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 216 Invalid, 57 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 57 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,954 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:27,958 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 40.
[2025-04-28 21:21:27,958 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 19 states have (on average 1.1578947368421053) internal successors, (22), 21 states have internal predecessors, (22), 8 states have call successors, (8), 6 states have call predecessors, (8), 12 states have return successors, (14), 12 states have call predecessors, (14), 8 states have call successors, (14)
[2025-04-28 21:21:27,959 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 44 transitions.
[2025-04-28 21:21:27,959 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 44 transitions. Word has length 37
[2025-04-28 21:21:27,959 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,959 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 44 transitions.
[2025-04-28 21:21:27,959 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 7 states have (on average 2.142857142857143) internal successors, (15), 10 states have internal predecessors, (15), 4 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:27,960 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 44 transitions.
[2025-04-28 21:21:27,961 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:21:27,961 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,961 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,967 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:28,162 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:28,163 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,163 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,163 INFO  L85        PathProgramCache]: Analyzing trace with hash 1567074762, now seen corresponding path program 2 times
[2025-04-28 21:21:28,163 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,163 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [253703040]
[2025-04-28 21:21:28,163 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,164 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,171 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:21:28,194 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:28,194 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,194 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,130 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 1 proven. 16 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:29,130 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,130 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [253703040]
[2025-04-28 21:21:29,130 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [253703040] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,130 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1539668591]
[2025-04-28 21:21:29,130 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:29,130 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,133 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,135 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,139 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,267 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:21:29,301 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:29,301 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:29,301 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,303 INFO  L256         TraceCheckSpWp]: Trace formula consists of 216 conjuncts, 51 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,306 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,735 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 10 proven. 6 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:29,736 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,270 INFO  L134       CoverageAnalysis]: Checked inductivity of 28 backedges. 10 proven. 8 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:32,270 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1539668591] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,270 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,270 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [19, 14, 16] total 33
[2025-04-28 21:21:32,270 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [260641434]
[2025-04-28 21:21:32,270 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,271 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-04-28 21:21:32,271 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,272 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-04-28 21:21:32,272 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=109, Invalid=947, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:32,273 INFO  L87              Difference]: Start difference. First operand 40 states and 44 transitions. Second operand  has 33 states, 21 states have (on average 2.0476190476190474) internal successors, (43), 33 states have internal predecessors, (43), 14 states have call successors, (18), 1 states have call predecessors, (18), 21 states have return successors, (29), 20 states have call predecessors, (29), 14 states have call successors, (29)
[2025-04-28 21:21:33,264 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,264 INFO  L93              Difference]: Finished difference Result 69 states and 77 transitions.
[2025-04-28 21:21:33,265 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 30 states. 
[2025-04-28 21:21:33,265 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 21 states have (on average 2.0476190476190474) internal successors, (43), 33 states have internal predecessors, (43), 14 states have call successors, (18), 1 states have call predecessors, (18), 21 states have return successors, (29), 20 states have call predecessors, (29), 14 states have call successors, (29) Word has length 49
[2025-04-28 21:21:33,265 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,266 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:33,266 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:21:33,268 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 144 GetRequests, 92 SyntacticMatches, 3 SemanticMatches, 49 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 396 ImplicationChecksByTransitivity, 1.3s TimeCoverageRelationStatistics Valid=258, Invalid=2292, Unknown=0, NotChecked=0, Total=2550
[2025-04-28 21:21:33,268 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 11 mSDsluCounter, 636 mSDsCounter, 0 mSdLazyCounter, 507 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 670 SdHoareTripleChecker+Invalid, 521 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 507 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,269 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 670 Invalid, 521 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 507 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:33,270 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:21:33,279 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 44.
[2025-04-28 21:21:33,279 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 21 states have (on average 1.1428571428571428) internal successors, (24), 23 states have internal predecessors, (24), 9 states have call successors, (9), 7 states have call predecessors, (9), 13 states have return successors, (15), 13 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:33,280 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 48 transitions.
[2025-04-28 21:21:33,280 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 48 transitions. Word has length 49
[2025-04-28 21:21:33,280 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,280 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 48 transitions.
[2025-04-28 21:21:33,281 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 21 states have (on average 2.0476190476190474) internal successors, (43), 33 states have internal predecessors, (43), 14 states have call successors, (18), 1 states have call predecessors, (18), 21 states have return successors, (29), 20 states have call predecessors, (29), 14 states have call successors, (29)
[2025-04-28 21:21:33,281 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 48 transitions.
[2025-04-28 21:21:33,282 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 54
[2025-04-28 21:21:33,282 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,282 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,288 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:33,486 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:33,486 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,487 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,487 INFO  L85        PathProgramCache]: Analyzing trace with hash 405079055, now seen corresponding path program 3 times
[2025-04-28 21:21:33,487 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,487 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [248760895]
[2025-04-28 21:21:33,487 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:33,488 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,495 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 53 statements into 4 equivalence classes.
[2025-04-28 21:21:33,506 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 53 of 53 statements.
[2025-04-28 21:21:33,506 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:33,506 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,890 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 7 proven. 18 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:33,890 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,890 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [248760895]
[2025-04-28 21:21:33,890 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [248760895] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,890 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [347159807]
[2025-04-28 21:21:33,891 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:33,891 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,893 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,895 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:33,899 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,031 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 53 statements into 4 equivalence classes.
[2025-04-28 21:21:34,068 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 53 of 53 statements.
[2025-04-28 21:21:34,068 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:34,068 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,070 INFO  L256         TraceCheckSpWp]: Trace formula consists of 236 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,072 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,157 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 12 proven. 10 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:21:34,159 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,831 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 12 proven. 14 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:38,831 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [347159807] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,831 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,831 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [19, 16, 19] total 25
[2025-04-28 21:21:38,831 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1028534999]
[2025-04-28 21:21:38,831 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,832 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:38,832 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,833 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:38,833 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=77, Invalid=523, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:38,833 INFO  L87              Difference]: Start difference. First operand 44 states and 48 transitions. Second operand  has 25 states, 14 states have (on average 2.2142857142857144) internal successors, (31), 25 states have internal predecessors, (31), 13 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (21), 13 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:39,148 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,148 INFO  L93              Difference]: Finished difference Result 62 states and 67 transitions.
[2025-04-28 21:21:39,149 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:39,149 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 14 states have (on average 2.2142857142857144) internal successors, (31), 25 states have internal predecessors, (31), 13 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (21), 13 states have call predecessors, (21), 13 states have call successors, (21) Word has length 53
[2025-04-28 21:21:39,149 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,150 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:39,150 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:39,150 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 132 GetRequests, 90 SyntacticMatches, 12 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 215 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=144, Invalid=848, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:39,151 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 16 mSDsluCounter, 393 mSDsCounter, 0 mSdLazyCounter, 197 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 423 SdHoareTripleChecker+Invalid, 215 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 197 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,151 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 423 Invalid, 215 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 197 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:39,152 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:39,162 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 50.
[2025-04-28 21:21:39,163 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 24 states have (on average 1.125) internal successors, (27), 26 states have internal predecessors, (27), 9 states have call successors, (9), 7 states have call predecessors, (9), 16 states have return successors, (18), 16 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:39,163 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 54 transitions.
[2025-04-28 21:21:39,167 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 54 transitions. Word has length 53
[2025-04-28 21:21:39,168 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,168 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 54 transitions.
[2025-04-28 21:21:39,168 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 14 states have (on average 2.2142857142857144) internal successors, (31), 25 states have internal predecessors, (31), 13 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (21), 13 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:39,168 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 54 transitions.
[2025-04-28 21:21:39,169 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-04-28 21:21:39,170 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,170 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,180 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:39,370 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,370 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,371 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,371 INFO  L85        PathProgramCache]: Analyzing trace with hash -360173735, now seen corresponding path program 4 times
[2025-04-28 21:21:39,371 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,371 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1988183813]
[2025-04-28 21:21:39,371 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:39,371 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,382 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 65 statements into 2 equivalence classes.
[2025-04-28 21:21:39,411 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:21:39,412 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:39,412 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,149 INFO  L134       CoverageAnalysis]: Checked inductivity of 66 backedges. 24 proven. 12 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:40,150 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1988183813]
[2025-04-28 21:21:40,150 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1988183813] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [324035548]
[2025-04-28 21:21:40,150 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:40,150 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,152 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,154 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:40,157 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,354 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 65 statements into 2 equivalence classes.
[2025-04-28 21:21:40,395 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:21:40,395 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:40,395 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,397 INFO  L256         TraceCheckSpWp]: Trace formula consists of 290 conjuncts, 68 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,400 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,929 INFO  L134       CoverageAnalysis]: Checked inductivity of 66 backedges. 6 proven. 12 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:40,929 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
