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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:51,672 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:51,779 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3b172f19-ab15-4f56-a3e3-d06365ed91b4/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:51,785 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:51,786 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:51,828 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:51,829 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:51,829 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:51,831 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:51,831 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:51,832 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:51,833 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:51,833 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:51,833 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:51,833 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:51,833 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:51,833 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:51,833 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:51,833 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:51,834 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:51,834 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:51,834 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:51,834 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:51,834 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:51,834 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:51,836 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:51,836 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:52,189 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:52,202 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:52,205 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:52,208 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:52,209 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:52,210 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3b172f19-ab15-4f56-a3e3-d06365ed91b4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-156.smt2
[2025-04-28 21:21:52,213 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:52,218 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:52,545 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3b172f19-ab15-4f56-a3e3-d06365ed91b4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-156.smt2
[2025-04-28 21:21:52,549 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:52,551 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:52,552 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:52,552 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:52,552 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:52,559 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,607 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52 Unit
[2025-04-28 21:21:52,607 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:52,608 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:52,608 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:52,609 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:52,635 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,635 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,671 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,672 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,677 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,679 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,681 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,683 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,684 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,711 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:52,715 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:52,715 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:52,715 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:52,716 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (1/1) ...
[2025-04-28 21:21:52,720 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:52,741 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,759 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:52,762 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:52,774 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:52,775 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:52,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:52,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_42 given in one single declaration
[2025-04-28 21:21:52,775 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_42
[2025-04-28 21:21:52,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_42
[2025-04-28 21:21:52,775 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:52,775 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:52,775 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:52,847 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:52,849 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:53,134 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:53,134 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:53,157 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:53,160 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:53,163 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53 BoogieIcfgContainer
[2025-04-28 21:21:53,163 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:53,166 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:53,170 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:53,175 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:53,175 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:52" (1/3) ...
[2025-04-28 21:21:53,176 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@c5452cd and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,176 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:52" (2/3) ...
[2025-04-28 21:21:53,176 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@c5452cd and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:53, skipping insertion in model container
[2025-04-28 21:21:53,176 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:53" (3/3) ...
[2025-04-28 21:21:53,178 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:53,194 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:53,196 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 24 locations, 56 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:53,254 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:53,269 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;@6c21334a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:53,270 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:53,279 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 24 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 12 states have internal predecessors, (14), 14 states have call successors, (14), 2 states have call predecessors, (14), 2 states have return successors, (14), 10 states have call predecessors, (14), 14 states have call successors, (14)
[2025-04-28 21:21:53,299 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:53,300 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,301 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,301 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,307 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,307 INFO  L85        PathProgramCache]: Analyzing trace with hash 1719832406, now seen corresponding path program 1 times
[2025-04-28 21:21:53,317 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,318 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [788012793]
[2025-04-28 21:21:53,318 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,319 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,357 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:53,422 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:53,422 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,422 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,102 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,104 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,105 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [788012793]
[2025-04-28 21:21:54,106 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [788012793] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,109 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [656228578]
[2025-04-28 21:21:54,109 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,110 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,115 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,120 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:54,122 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,193 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:54,244 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:54,244 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,244 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,252 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,259 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,458 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,459 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,903 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,903 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [656228578] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,904 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,909 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 9
[2025-04-28 21:21:54,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [936408997]
[2025-04-28 21:21:54,912 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,917 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:54,917 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,004 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:55,006 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:55,021 INFO  L87              Difference]: Start difference. First operand  has 24 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 12 states have internal predecessors, (14), 14 states have call successors, (14), 2 states have call predecessors, (14), 2 states have return successors, (14), 10 states have call predecessors, (14), 14 states have call successors, (14) Second operand  has 9 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 5 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:55,559 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,560 INFO  L93              Difference]: Finished difference Result 27 states and 58 transitions.
[2025-04-28 21:21:55,562 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:55,564 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 5 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5) Word has length 13
[2025-04-28 21:21:55,564 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,576 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:55,577 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:55,580 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 24 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=30, Invalid=80, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:55,587 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 3 mSDsluCounter, 106 mSDsCounter, 0 mSdLazyCounter, 142 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 136 SdHoareTripleChecker+Invalid, 153 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 142 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,588 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 136 Invalid, 153 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 142 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:55,607 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:55,656 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 25.
[2025-04-28 21:21:55,658 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 15 states have call successors, (15), 2 states have call predecessors, (15), 3 states have return successors, (28), 11 states have call predecessors, (28), 15 states have call successors, (28)
[2025-04-28 21:21:55,667 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 56 transitions.
[2025-04-28 21:21:55,669 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 56 transitions. Word has length 13
[2025-04-28 21:21:55,670 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,671 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 56 transitions.
[2025-04-28 21:21:55,671 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 5 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:55,671 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 56 transitions.
[2025-04-28 21:21:55,677 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:55,679 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,679 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,686 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:55,884 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,884 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,885 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,885 INFO  L85        PathProgramCache]: Analyzing trace with hash 1677850780, now seen corresponding path program 1 times
[2025-04-28 21:21:55,885 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,885 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [501882128]
[2025-04-28 21:21:55,886 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,886 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,896 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:55,907 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:55,907 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,907 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,178 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:56,178 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,178 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [501882128]
[2025-04-28 21:21:56,178 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [501882128] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,179 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [540452578]
[2025-04-28 21:21:56,179 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,179 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,183 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,185 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:56,190 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,253 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:56,293 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:56,293 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,293 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,300 INFO  L256         TraceCheckSpWp]: Trace formula consists of 162 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,302 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,521 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:56,521 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,992 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:56,992 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [540452578] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,992 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,992 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:56,992 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [66791728]
[2025-04-28 21:21:56,992 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,993 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:56,993 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,994 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:56,994 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=232, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:56,994 INFO  L87              Difference]: Start difference. First operand 25 states and 56 transitions. Second operand  has 17 states, 8 states have (on average 2.25) internal successors, (18), 13 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 6 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:58,372 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,372 INFO  L93              Difference]: Finished difference Result 51 states and 177 transitions.
[2025-04-28 21:21:58,373 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:58,373 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.25) internal successors, (18), 13 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 6 states have call predecessors, (10), 10 states have call successors, (10) Word has length 17
[2025-04-28 21:21:58,373 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,377 INFO  L225             Difference]: With dead ends: 51
[2025-04-28 21:21:58,380 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:58,381 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 24 SyntacticMatches, 2 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 58 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=103, Invalid=497, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:58,383 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 24 mSDsluCounter, 183 mSDsCounter, 0 mSdLazyCounter, 933 mSolverCounterSat, 76 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 56 SdHoareTripleChecker+Valid, 221 SdHoareTripleChecker+Invalid, 1009 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 76 IncrementalHoareTripleChecker+Valid, 933 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,383 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [56 Valid, 221 Invalid, 1009 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [76 Valid, 933 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:58,384 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:58,430 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 41.
[2025-04-28 21:21:58,431 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 9 states have (on average 2.5555555555555554) internal successors, (23), 18 states have internal predecessors, (23), 26 states have call successors, (26), 3 states have call predecessors, (26), 5 states have return successors, (72), 19 states have call predecessors, (72), 26 states have call successors, (72)
[2025-04-28 21:21:58,433 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 121 transitions.
[2025-04-28 21:21:58,433 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 121 transitions. Word has length 17
[2025-04-28 21:21:58,434 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,434 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 121 transitions.
[2025-04-28 21:21:58,434 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.25) internal successors, (18), 13 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 6 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:58,434 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 121 transitions.
[2025-04-28 21:21:58,437 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:58,437 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,437 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,444 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:58,641 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,641 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,642 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,642 INFO  L85        PathProgramCache]: Analyzing trace with hash -1554621540, now seen corresponding path program 2 times
[2025-04-28 21:21:58,642 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,642 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1965407977]
[2025-04-28 21:21:58,642 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:58,642 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,650 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:58,659 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:58,659 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:58,659 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,875 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:58,875 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,875 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1965407977]
[2025-04-28 21:21:58,875 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1965407977] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,875 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [869241884]
[2025-04-28 21:21:58,876 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:58,876 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,878 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,880 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:58,883 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,929 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:58,956 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:58,957 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:58,957 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,959 INFO  L256         TraceCheckSpWp]: Trace formula consists of 162 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,961 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:59,123 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:59,123 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,833 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:59,833 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [869241884] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,833 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,833 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 6, 6] total 14
[2025-04-28 21:21:59,834 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [44223158]
[2025-04-28 21:21:59,834 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,834 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:59,834 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,835 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:59,835 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=153, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:59,836 INFO  L87              Difference]: Start difference. First operand 41 states and 121 transitions. Second operand  has 14 states, 7 states have (on average 2.857142857142857) internal successors, (20), 13 states have internal predecessors, (20), 9 states have call successors, (10), 2 states have call predecessors, (10), 7 states have return successors, (10), 4 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:22:00,651 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,651 INFO  L93              Difference]: Finished difference Result 57 states and 227 transitions.
[2025-04-28 21:22:00,651 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:00,652 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.857142857142857) internal successors, (20), 13 states have internal predecessors, (20), 9 states have call successors, (10), 2 states have call predecessors, (10), 7 states have return successors, (10), 4 states have call predecessors, (10), 9 states have call successors, (10) Word has length 17
[2025-04-28 21:22:00,652 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,655 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:22:00,655 INFO  L226             Difference]: Without dead ends: 57
[2025-04-28 21:22:00,655 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 33 SyntacticMatches, 0 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 19 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=67, Invalid=313, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:22:00,656 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 11 mSDsluCounter, 159 mSDsCounter, 0 mSdLazyCounter, 524 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 191 SdHoareTripleChecker+Invalid, 549 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 524 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,656 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 191 Invalid, 549 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 524 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:00,657 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 57 states.
[2025-04-28 21:22:00,681 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 57 to 41.
[2025-04-28 21:22:00,681 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 9 states have (on average 2.5555555555555554) internal successors, (23), 18 states have internal predecessors, (23), 26 states have call successors, (26), 3 states have call predecessors, (26), 5 states have return successors, (71), 19 states have call predecessors, (71), 26 states have call successors, (71)
[2025-04-28 21:22:00,683 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 120 transitions.
[2025-04-28 21:22:00,683 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 120 transitions. Word has length 17
[2025-04-28 21:22:00,683 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,683 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 120 transitions.
[2025-04-28 21:22:00,683 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.857142857142857) internal successors, (20), 13 states have internal predecessors, (20), 9 states have call successors, (10), 2 states have call predecessors, (10), 7 states have return successors, (10), 4 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:22:00,683 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 120 transitions.
[2025-04-28 21:22:00,686 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:22:00,686 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,686 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,692 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:00,890 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,890 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,891 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,891 INFO  L85        PathProgramCache]: Analyzing trace with hash -132321055, now seen corresponding path program 1 times
[2025-04-28 21:22:00,891 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,891 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1098387254]
[2025-04-28 21:22:00,891 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,891 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,898 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:22:00,921 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:00,925 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,925 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,200 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 4 proven. 14 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:01,201 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,201 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1098387254]
[2025-04-28 21:22:01,201 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1098387254] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,201 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [867563714]
[2025-04-28 21:22:01,201 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,201 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,203 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,206 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:22:01,209 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,260 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:22:01,306 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:01,306 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,306 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,308 INFO  L256         TraceCheckSpWp]: Trace formula consists of 274 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,310 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,354 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:01,354 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:01,355 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [867563714] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,355 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:01,355 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [9] total 11
[2025-04-28 21:22:01,355 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [14771628]
[2025-04-28 21:22:01,355 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,355 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:01,355 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,356 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:01,356 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:01,356 INFO  L87              Difference]: Start difference. First operand 41 states and 120 transitions. 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, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:01,466 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,466 INFO  L93              Difference]: Finished difference Result 49 states and 172 transitions.
[2025-04-28 21:22:01,467 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:01,467 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, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 25
[2025-04-28 21:22:01,467 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,469 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:22:01,469 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:22:01,473 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 34 GetRequests, 25 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:01,474 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 1 mSDsluCounter, 63 mSDsCounter, 0 mSdLazyCounter, 59 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 117 SdHoareTripleChecker+Invalid, 60 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 59 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,474 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 117 Invalid, 60 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 59 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,475 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:22:01,494 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 43.
[2025-04-28 21:22:01,495 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 43 states, 10 states have (on average 2.4) internal successors, (24), 19 states have internal predecessors, (24), 26 states have call successors, (26), 3 states have call predecessors, (26), 6 states have return successors, (93), 20 states have call predecessors, (93), 26 states have call successors, (93)
[2025-04-28 21:22:01,505 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 43 states to 43 states and 143 transitions.
[2025-04-28 21:22:01,505 INFO  L79                 Accepts]: Start accepts. Automaton has 43 states and 143 transitions. Word has length 25
[2025-04-28 21:22:01,505 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,506 INFO  L485      AbstractCegarLoop]: Abstraction has 43 states and 143 transitions.
[2025-04-28 21:22:01,506 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, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:01,506 INFO  L278                IsEmpty]: Start isEmpty. Operand 43 states and 143 transitions.
[2025-04-28 21:22:01,509 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:22:01,509 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,509 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,515 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:01,710 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,710 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,711 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,711 INFO  L85        PathProgramCache]: Analyzing trace with hash 895877287, now seen corresponding path program 1 times
[2025-04-28 21:22:01,711 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,711 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [820399614]
[2025-04-28 21:22:01,711 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,711 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,718 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:22:01,732 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:01,732 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,967 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 4 proven. 14 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:01,967 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [820399614]
[2025-04-28 21:22:01,967 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [820399614] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [169763078]
[2025-04-28 21:22:01,967 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,968 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,970 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,972 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:22:01,976 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:22:02,071 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:02,071 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,071 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,073 INFO  L256         TraceCheckSpWp]: Trace formula consists of 274 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,075 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,269 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 4 proven. 16 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:22:02,269 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:02,837 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 4 proven. 16 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:22:02,838 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [169763078] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:02,838 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:02,838 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 10, 10] total 21
[2025-04-28 21:22:02,838 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1983246444]
[2025-04-28 21:22:02,838 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,838 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:22:02,838 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,839 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:22:02,839 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=51, Invalid=369, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:22:02,840 INFO  L87              Difference]: Start difference. First operand 43 states and 143 transitions. Second operand  has 21 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 15 states have call successors, (15), 1 states have call predecessors, (15), 9 states have return successors, (15), 7 states have call predecessors, (15), 15 states have call successors, (15)
[2025-04-28 21:22:05,411 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,412 INFO  L93              Difference]: Finished difference Result 69 states and 322 transitions.
[2025-04-28 21:22:05,412 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:22:05,413 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 15 states have call successors, (15), 1 states have call predecessors, (15), 9 states have return successors, (15), 7 states have call predecessors, (15), 15 states have call successors, (15) Word has length 25
[2025-04-28 21:22:05,413 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,418 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:22:05,418 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:22:05,419 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 84 GetRequests, 48 SyntacticMatches, 3 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 139 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=164, Invalid=1026, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:22:05,420 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 26 mSDsluCounter, 214 mSDsCounter, 0 mSdLazyCounter, 1806 mSolverCounterSat, 121 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 60 SdHoareTripleChecker+Valid, 258 SdHoareTripleChecker+Invalid, 1927 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 121 IncrementalHoareTripleChecker+Valid, 1806 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,420 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [60 Valid, 258 Invalid, 1927 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [121 Valid, 1806 Invalid, 0 Unknown, 0 Unchecked, 2.1s Time]
[2025-04-28 21:22:05,425 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:22:05,479 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 46.
[2025-04-28 21:22:05,483 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 11 states have (on average 2.272727272727273) internal successors, (25), 20 states have internal predecessors, (25), 27 states have call successors, (27), 3 states have call predecessors, (27), 7 states have return successors, (120), 22 states have call predecessors, (120), 27 states have call successors, (120)
[2025-04-28 21:22:05,485 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 172 transitions.
[2025-04-28 21:22:05,488 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 172 transitions. Word has length 25
[2025-04-28 21:22:05,489 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,489 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 172 transitions.
[2025-04-28 21:22:05,489 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 15 states have call successors, (15), 1 states have call predecessors, (15), 9 states have return successors, (15), 7 states have call predecessors, (15), 15 states have call successors, (15)
[2025-04-28 21:22:05,489 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 172 transitions.
[2025-04-28 21:22:05,492 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:05,495 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,495 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,503 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:05,695 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,696 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,696 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,696 INFO  L85        PathProgramCache]: Analyzing trace with hash -380173221, now seen corresponding path program 1 times
[2025-04-28 21:22:05,696 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,697 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [921370868]
[2025-04-28 21:22:05,697 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,697 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,703 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:05,717 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:05,717 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:05,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,002 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:06,003 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,003 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [921370868]
[2025-04-28 21:22:06,003 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [921370868] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,003 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1421466842]
[2025-04-28 21:22:06,003 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,003 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,006 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,009 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:22:06,013 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,071 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:06,114 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:06,114 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,114 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,121 INFO  L256         TraceCheckSpWp]: Trace formula consists of 224 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,125 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:06,267 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 11 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,267 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:07,019 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 8 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:07,020 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1421466842] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:07,020 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:07,020 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 6, 6] total 14
[2025-04-28 21:22:07,020 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1731497764]
[2025-04-28 21:22:07,020 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,021 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:22:07,021 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,021 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:22:07,022 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=153, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:07,022 INFO  L87              Difference]: Start difference. First operand 46 states and 172 transitions. Second operand  has 14 states, 7 states have (on average 2.857142857142857) internal successors, (20), 13 states have internal predecessors, (20), 11 states have call successors, (12), 2 states have call predecessors, (12), 7 states have return successors, (12), 4 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:22:07,553 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,553 INFO  L93              Difference]: Finished difference Result 58 states and 241 transitions.
[2025-04-28 21:22:07,554 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:22:07,554 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.857142857142857) internal successors, (20), 13 states have internal predecessors, (20), 11 states have call successors, (12), 2 states have call predecessors, (12), 7 states have return successors, (12), 4 states have call predecessors, (12), 11 states have call successors, (12) Word has length 21
[2025-04-28 21:22:07,554 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,557 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:22:07,557 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:22:07,557 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 57 GetRequests, 40 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=60, Invalid=282, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:07,558 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 12 mSDsluCounter, 108 mSDsCounter, 0 mSdLazyCounter, 319 mSolverCounterSat, 40 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 136 SdHoareTripleChecker+Invalid, 359 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 40 IncrementalHoareTripleChecker+Valid, 319 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,559 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 136 Invalid, 359 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [40 Valid, 319 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:07,559 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:22:07,594 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 49.
[2025-04-28 21:22:07,595 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 49 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 21 states have internal predecessors, (26), 28 states have call successors, (28), 3 states have call predecessors, (28), 8 states have return successors, (148), 24 states have call predecessors, (148), 28 states have call successors, (148)
[2025-04-28 21:22:07,600 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 49 states to 49 states and 202 transitions.
[2025-04-28 21:22:07,600 INFO  L79                 Accepts]: Start accepts. Automaton has 49 states and 202 transitions. Word has length 21
[2025-04-28 21:22:07,601 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,601 INFO  L485      AbstractCegarLoop]: Abstraction has 49 states and 202 transitions.
[2025-04-28 21:22:07,601 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.857142857142857) internal successors, (20), 13 states have internal predecessors, (20), 11 states have call successors, (12), 2 states have call predecessors, (12), 7 states have return successors, (12), 4 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:22:07,601 INFO  L278                IsEmpty]: Start isEmpty. Operand 49 states and 202 transitions.
[2025-04-28 21:22:07,607 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:07,607 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,607 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,614 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:07,811 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,811 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,812 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,812 INFO  L85        PathProgramCache]: Analyzing trace with hash -1029414181, now seen corresponding path program 2 times
[2025-04-28 21:22:07,812 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,812 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [69384173]
[2025-04-28 21:22:07,812 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:07,813 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,820 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:22:07,833 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:07,834 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:07,834 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,078 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:08,079 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,079 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [69384173]
[2025-04-28 21:22:08,079 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [69384173] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:08,079 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1988365275]
[2025-04-28 21:22:08,079 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:08,079 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,082 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:08,085 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:08,089 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:08,150 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:22:08,188 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:08,189 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:08,189 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,190 INFO  L256         TraceCheckSpWp]: Trace formula consists of 224 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:08,192 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,286 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:08,286 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,553 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:08,553 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1988365275] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,553 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,553 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 15
[2025-04-28 21:22:08,554 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [823872295]
[2025-04-28 21:22:08,554 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,554 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:22:08,554 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,555 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:22:08,555 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=175, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:22:08,556 INFO  L87              Difference]: Start difference. First operand 49 states and 202 transitions. Second operand  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 11 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:22:09,559 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,559 INFO  L93              Difference]: Finished difference Result 80 states and 335 transitions.
[2025-04-28 21:22:09,560 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:09,560 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 11 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 11 states have call successors, (11) Word has length 21
[2025-04-28 21:22:09,560 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,563 INFO  L225             Difference]: With dead ends: 80
[2025-04-28 21:22:09,563 INFO  L226             Difference]: Without dead ends: 80
[2025-04-28 21:22:09,563 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 35 SyntacticMatches, 4 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 56 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=77, Invalid=343, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:22:09,564 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 16 mSDsluCounter, 149 mSDsCounter, 0 mSdLazyCounter, 909 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 188 SdHoareTripleChecker+Invalid, 943 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 909 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,564 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 188 Invalid, 943 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 909 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:09,565 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 80 states.
[2025-04-28 21:22:09,589 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 80 to 63.
[2025-04-28 21:22:09,590 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 14 states have (on average 2.5) internal successors, (35), 27 states have internal predecessors, (35), 39 states have call successors, (39), 4 states have call predecessors, (39), 9 states have return successors, (202), 31 states have call predecessors, (202), 39 states have call successors, (202)
[2025-04-28 21:22:09,592 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 276 transitions.
[2025-04-28 21:22:09,593 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 276 transitions. Word has length 21
[2025-04-28 21:22:09,593 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,593 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 276 transitions.
[2025-04-28 21:22:09,593 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 11 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:22:09,593 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 276 transitions.
[2025-04-28 21:22:09,597 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:09,597 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,597 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:09,603 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:09,801 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable7
[2025-04-28 21:22:09,801 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,802 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,802 INFO  L85        PathProgramCache]: Analyzing trace with hash -124044639, now seen corresponding path program 1 times
[2025-04-28 21:22:09,802 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,802 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [293624264]
[2025-04-28 21:22:09,802 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,802 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,808 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:09,815 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:09,815 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,815 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,959 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:09,959 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,959 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [293624264]
[2025-04-28 21:22:09,959 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [293624264] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,959 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1364723280]
[2025-04-28 21:22:09,960 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,960 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,963 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,965 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:09,972 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:10,032 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:10,070 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:10,071 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,071 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,072 INFO  L256         TraceCheckSpWp]: Trace formula consists of 224 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:10,074 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,184 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:10,185 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:10,469 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:10,470 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1364723280] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:10,470 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:10,470 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 16
[2025-04-28 21:22:10,470 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1560884011]
[2025-04-28 21:22:10,470 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:10,471 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:22:10,471 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:10,471 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:22:10,471 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=205, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:22:10,472 INFO  L87              Difference]: Start difference. First operand 63 states and 276 transitions. Second operand  has 16 states, 8 states have (on average 2.5) internal successors, (20), 14 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 5 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:22:11,889 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:11,889 INFO  L93              Difference]: Finished difference Result 136 states and 703 transitions.
[2025-04-28 21:22:11,889 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:11,890 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.5) internal successors, (20), 14 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 5 states have call predecessors, (11), 11 states have call successors, (11) Word has length 21
[2025-04-28 21:22:11,890 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:11,896 INFO  L225             Difference]: With dead ends: 136
[2025-04-28 21:22:11,896 INFO  L226             Difference]: Without dead ends: 136
[2025-04-28 21:22:11,896 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 62 GetRequests, 36 SyntacticMatches, 4 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 51 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=92, Invalid=460, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:11,897 INFO  L437           NwaCegarLoop]: 45 mSDtfsCounter, 40 mSDsluCounter, 231 mSDsCounter, 0 mSdLazyCounter, 1217 mSolverCounterSat, 176 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 58 SdHoareTripleChecker+Valid, 276 SdHoareTripleChecker+Invalid, 1393 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 176 IncrementalHoareTripleChecker+Valid, 1217 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:11,897 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [58 Valid, 276 Invalid, 1393 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [176 Valid, 1217 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:22:11,898 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 136 states.
[2025-04-28 21:22:11,982 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 136 to 97.
[2025-04-28 21:22:11,986 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 97 states, 20 states have (on average 2.45) internal successors, (49), 41 states have internal predecessors, (49), 63 states have call successors, (63), 6 states have call predecessors, (63), 13 states have return successors, (448), 49 states have call predecessors, (448), 63 states have call successors, (448)
[2025-04-28 21:22:11,990 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 97 states to 97 states and 560 transitions.
[2025-04-28 21:22:11,990 INFO  L79                 Accepts]: Start accepts. Automaton has 97 states and 560 transitions. Word has length 21
[2025-04-28 21:22:11,990 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:11,990 INFO  L485      AbstractCegarLoop]: Abstraction has 97 states and 560 transitions.
[2025-04-28 21:22:11,990 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.5) internal successors, (20), 14 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 5 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:22:11,991 INFO  L278                IsEmpty]: Start isEmpty. Operand 97 states and 560 transitions.
[2025-04-28 21:22:11,997 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:22:11,997 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:11,997 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,003 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:12,201 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:12,201 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,202 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,203 INFO  L85        PathProgramCache]: Analyzing trace with hash 928738151, now seen corresponding path program 2 times
[2025-04-28 21:22:12,203 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,203 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [389934684]
[2025-04-28 21:22:12,203 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:12,203 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,208 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:22:12,220 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:12,220 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:12,220 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,416 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 8 proven. 10 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:12,416 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:12,416 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [389934684]
[2025-04-28 21:22:12,416 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [389934684] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:12,416 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [312334077]
[2025-04-28 21:22:12,417 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:12,417 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:12,419 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:12,422 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:12,426 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:12,489 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:22:12,537 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:12,537 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:12,537 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,539 INFO  L256         TraceCheckSpWp]: Trace formula consists of 274 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:12,541 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:12,587 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 20 proven. 0 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:22:12,587 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:12,587 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [312334077] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:12,587 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:12,587 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [8] total 10
[2025-04-28 21:22:12,587 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1645572506]
[2025-04-28 21:22:12,588 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,590 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:12,590 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,591 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:12,591 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:22:12,591 INFO  L87              Difference]: Start difference. First operand 97 states and 560 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 4 states have call successors, (6), 2 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:22:12,709 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,709 INFO  L93              Difference]: Finished difference Result 115 states and 677 transitions.
[2025-04-28 21:22:12,713 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:12,713 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 4 states have call successors, (6), 2 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 25
[2025-04-28 21:22:12,714 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,721 INFO  L225             Difference]: With dead ends: 115
[2025-04-28 21:22:12,721 INFO  L226             Difference]: Without dead ends: 115
[2025-04-28 21:22:12,721 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 24 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:22:12,724 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 1 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 59 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 130 SdHoareTripleChecker+Invalid, 59 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 59 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,724 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 130 Invalid, 59 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 59 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:12,725 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 115 states.
[2025-04-28 21:22:12,789 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 115 to 99.
[2025-04-28 21:22:12,791 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 21 states have (on average 2.380952380952381) internal successors, (50), 42 states have internal predecessors, (50), 63 states have call successors, (63), 6 states have call predecessors, (63), 14 states have return successors, (490), 50 states have call predecessors, (490), 63 states have call successors, (490)
[2025-04-28 21:22:12,794 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 603 transitions.
[2025-04-28 21:22:12,795 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 603 transitions. Word has length 25
[2025-04-28 21:22:12,795 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,795 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 603 transitions.
[2025-04-28 21:22:12,796 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 4 states have call successors, (6), 2 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:22:12,796 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 603 transitions.
[2025-04-28 21:22:12,805 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:22:12,805 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,805 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,812 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:13,006 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:13,006 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,006 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,006 INFO  L85        PathProgramCache]: Analyzing trace with hash -1451651866, now seen corresponding path program 1 times
[2025-04-28 21:22:13,007 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,007 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [754412184]
[2025-04-28 21:22:13,007 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,007 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,013 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:22:13,045 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:22:13,045 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,045 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,232 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 12 proven. 12 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:22:13,232 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,232 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [754412184]
[2025-04-28 21:22:13,232 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [754412184] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:13,232 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1887554714]
[2025-04-28 21:22:13,233 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,233 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,236 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:13,238 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:13,243 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:13,313 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:22:13,370 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:22:13,370 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,370 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,375 INFO  L256         TraceCheckSpWp]: Trace formula consists of 336 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:13,377 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:13,428 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 27 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:13,428 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:13,428 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1887554714] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:13,428 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:13,429 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [8] total 10
[2025-04-28 21:22:13,429 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [885521348]
[2025-04-28 21:22:13,429 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,429 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:13,429 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,430 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:13,430 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:22:13,430 INFO  L87              Difference]: Start difference. First operand 99 states and 603 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 4 states have call successors, (7), 2 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:22:13,640 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,641 INFO  L93              Difference]: Finished difference Result 100 states and 571 transitions.
[2025-04-28 21:22:13,641 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:13,641 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 4 states have call successors, (7), 2 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7) Word has length 29
[2025-04-28 21:22:13,642 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,646 INFO  L225             Difference]: With dead ends: 100
[2025-04-28 21:22:13,646 INFO  L226             Difference]: Without dead ends: 100
[2025-04-28 21:22:13,647 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=87, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:13,647 INFO  L437           NwaCegarLoop]: 41 mSDtfsCounter, 1 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 90 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 84 SdHoareTripleChecker+Invalid, 96 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 90 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,648 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 84 Invalid, 96 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 90 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:13,648 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 100 states.
[2025-04-28 21:22:13,700 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 100 to 86.
[2025-04-28 21:22:13,701 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 86 states, 20 states have (on average 2.25) internal successors, (45), 38 states have internal predecessors, (45), 51 states have call successors, (51), 5 states have call predecessors, (51), 14 states have return successors, (418), 42 states have call predecessors, (418), 51 states have call successors, (418)
[2025-04-28 21:22:13,704 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 86 states to 86 states and 514 transitions.
[2025-04-28 21:22:13,704 INFO  L79                 Accepts]: Start accepts. Automaton has 86 states and 514 transitions. Word has length 29
[2025-04-28 21:22:13,705 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,705 INFO  L485      AbstractCegarLoop]: Abstraction has 86 states and 514 transitions.
[2025-04-28 21:22:13,705 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 4 states have call successors, (7), 2 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:22:13,705 INFO  L278                IsEmpty]: Start isEmpty. Operand 86 states and 514 transitions.
[2025-04-28 21:22:13,711 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:22:13,712 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,712 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,718 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:22:13,912 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,912 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,913 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,913 INFO  L85        PathProgramCache]: Analyzing trace with hash -1351553962, now seen corresponding path program 1 times
[2025-04-28 21:22:13,913 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,913 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1690443589]
[2025-04-28 21:22:13,913 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,913 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,920 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:22:13,934 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:22:13,934 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,934 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,188 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 10 proven. 18 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:22:14,189 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:14,189 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1690443589]
[2025-04-28 21:22:14,189 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1690443589] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:14,189 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [224977521]
[2025-04-28 21:22:14,189 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:14,189 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:14,195 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:14,198 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:14,202 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:22:14,276 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:22:14,333 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:22:14,333 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:14,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,335 INFO  L256         TraceCheckSpWp]: Trace formula consists of 335 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:14,337 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:14,503 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 12 proven. 14 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:22:14,503 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:15,066 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 12 proven. 14 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:22:15,066 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [224977521] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:15,066 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:15,067 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 20
[2025-04-28 21:22:15,067 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [8701335]
[2025-04-28 21:22:15,067 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:15,067 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:22:15,068 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:15,070 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:22:15,070 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=334, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:22:15,070 INFO  L87              Difference]: Start difference. First operand 86 states and 514 transitions. Second operand  has 20 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 14 states have call successors, (16), 1 states have call predecessors, (16), 9 states have return successors, (16), 7 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:22:20,292 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:20,293 INFO  L93              Difference]: Finished difference Result 275 states and 2280 transitions.
[2025-04-28 21:22:20,293 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 34 states. 
[2025-04-28 21:22:20,294 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 14 states have call successors, (16), 1 states have call predecessors, (16), 9 states have return successors, (16), 7 states have call predecessors, (16), 14 states have call successors, (16) Word has length 29
[2025-04-28 21:22:20,294 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:20,314 INFO  L225             Difference]: With dead ends: 275
[2025-04-28 21:22:20,314 INFO  L226             Difference]: Without dead ends: 245
[2025-04-28 21:22:20,315 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 125 GetRequests, 72 SyntacticMatches, 5 SemanticMatches, 48 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 457 ImplicationChecksByTransitivity, 1.2s TimeCoverageRelationStatistics Valid=335, Invalid=2115, Unknown=0, NotChecked=0, Total=2450
[2025-04-28 21:22:20,316 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 53 mSDsluCounter, 266 mSDsCounter, 0 mSdLazyCounter, 4079 mSolverCounterSat, 293 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 3.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 76 SdHoareTripleChecker+Valid, 323 SdHoareTripleChecker+Invalid, 4372 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 293 IncrementalHoareTripleChecker+Valid, 4079 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 4.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:20,316 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [76 Valid, 323 Invalid, 4372 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [293 Valid, 4079 Invalid, 0 Unknown, 0 Unchecked, 4.2s Time]
[2025-04-28 21:22:20,317 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 245 states.
[2025-04-28 21:22:20,571 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 245 to 117.
[2025-04-28 21:22:20,572 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 27 states have (on average 2.259259259259259) internal successors, (61), 51 states have internal predecessors, (61), 70 states have call successors, (70), 7 states have call predecessors, (70), 19 states have return successors, (510), 58 states have call predecessors, (510), 70 states have call successors, (510)
[2025-04-28 21:22:20,577 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 641 transitions.
[2025-04-28 21:22:20,577 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 641 transitions. Word has length 29
[2025-04-28 21:22:20,577 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:20,578 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 641 transitions.
[2025-04-28 21:22:20,578 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 14 states have call successors, (16), 1 states have call predecessors, (16), 9 states have return successors, (16), 7 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:22:20,578 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 641 transitions.
[2025-04-28 21:22:20,587 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:22:20,587 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:20,587 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:20,594 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:20,788 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:22:20,788 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:20,789 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:20,790 INFO  L85        PathProgramCache]: Analyzing trace with hash 799971233, now seen corresponding path program 2 times
[2025-04-28 21:22:20,790 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:20,790 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [675530649]
[2025-04-28 21:22:20,790 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:20,790 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:20,796 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:22:20,803 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:20,803 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:20,803 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:20,929 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 6 proven. 14 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:22:20,929 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:20,929 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [675530649]
[2025-04-28 21:22:20,929 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [675530649] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:20,929 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1841240919]
[2025-04-28 21:22:20,929 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:20,930 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:20,932 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:20,934 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:20,937 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
