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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:37,525 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:37,624 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7f083c0b-8c95-466c-92ed-63a80711d2e4/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:37,632 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:37,632 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:37,655 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:37,656 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:37,656 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:37,656 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:37,656 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:37,657 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:37,657 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:37,657 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:37,658 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:37,658 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:37,659 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:37,659 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:37,659 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:37,660 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:37,661 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:37,662 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:38,012 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:38,024 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:38,026 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:38,028 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:38,030 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:38,032 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7f083c0b-8c95-466c-92ed-63a80711d2e4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-003.smt2
[2025-04-28 21:21:38,034 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:38,041 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:38,294 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7f083c0b-8c95-466c-92ed-63a80711d2e4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-003.smt2
[2025-04-28 21:21:38,301 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:38,302 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:38,305 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:38,305 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:38,306 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:38,308 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,338 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38 Unit
[2025-04-28 21:21:38,339 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:38,340 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:38,341 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:38,341 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:38,358 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,358 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,397 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,397 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,400 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,401 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,405 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,406 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,406 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,427 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:38,428 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:38,428 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:38,428 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:38,429 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (1/1) ...
[2025-04-28 21:21:38,432 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:38,447 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,463 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:38,467 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:38,480 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:38,480 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:38,480 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:38,480 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry.split given in one single declaration
[2025-04-28 21:21:38,480 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry.split
[2025-04-28 21:21:38,480 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry.split
[2025-04-28 21:21:38,481 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo given in one single declaration
[2025-04-28 21:21:38,481 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo
[2025-04-28 21:21:38,481 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo
[2025-04-28 21:21:38,481 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo.ATUnifiedReturnBlock.split given in one single declaration
[2025-04-28 21:21:38,481 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo.ATUnifiedReturnBlock.split
[2025-04-28 21:21:38,481 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo.ATUnifiedReturnBlock.split
[2025-04-28 21:21:38,481 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo.AT_tail given in one single declaration
[2025-04-28 21:21:38,481 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo.AT_tail
[2025-04-28 21:21:38,481 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo.AT_tail
[2025-04-28 21:21:38,481 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:38,481 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:38,481 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:38,481 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:38,482 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:38,482 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:38,549 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:38,552 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:38,695 INFO  L?                        ?]: Removed 19 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:38,695 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:38,711 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:38,712 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:38,712 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:38 BoogieIcfgContainer
[2025-04-28 21:21:38,712 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:38,719 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:38,719 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:38,725 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:38,725 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:38" (1/3) ...
[2025-04-28 21:21:38,726 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@12a9c731 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:38, skipping insertion in model container
[2025-04-28 21:21:38,726 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:38" (2/3) ...
[2025-04-28 21:21:38,726 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@12a9c731 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:38, skipping insertion in model container
[2025-04-28 21:21:38,726 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:38" (3/3) ...
[2025-04-28 21:21:38,729 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:38,746 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:38,750 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 27 locations, 39 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:38,807 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:38,829 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;@11fedc7, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:38,829 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:38,834 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 27 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 8 states have call predecessors, (8), 8 states have call successors, (8)
[2025-04-28 21:21:38,844 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:38,844 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,845 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,845 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,851 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,852 INFO  L85        PathProgramCache]: Analyzing trace with hash 337092792, now seen corresponding path program 1 times
[2025-04-28 21:21:38,862 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,862 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1560857381]
[2025-04-28 21:21:38,862 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,863 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,892 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:38,911 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:38,913 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,915 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,059 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:39,060 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,060 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1560857381]
[2025-04-28 21:21:39,061 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1560857381] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,061 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,065 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:39,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [170972112]
[2025-04-28 21:21:39,070 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,075 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,076 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,113 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,114 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,116 INFO  L87              Difference]: Start difference. First operand  has 27 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 8 states have call predecessors, (8), 8 states have call successors, (8) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:39,193 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,193 INFO  L93              Difference]: Finished difference Result 27 states and 32 transitions.
[2025-04-28 21:21:39,196 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:39,198 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:39,198 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,206 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:39,207 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:39,210 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,214 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 70 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,215 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 70 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:39,232 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:39,272 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:39,273 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 13 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:39,280 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:39,281 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:39,282 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,283 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:39,283 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:39,283 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:39,285 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:39,285 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,285 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,286 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:39,286 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,287 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,288 INFO  L85        PathProgramCache]: Analyzing trace with hash -1281600460, now seen corresponding path program 1 times
[2025-04-28 21:21:39,288 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,288 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1723637343]
[2025-04-28 21:21:39,288 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,288 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,299 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:39,311 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:39,311 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,311 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,398 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:39,398 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,398 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1723637343]
[2025-04-28 21:21:39,398 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1723637343] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,399 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:39,399 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [931770741]
[2025-04-28 21:21:39,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,400 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,403 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,404 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,404 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,405 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:39,461 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,461 INFO  L93              Difference]: Finished difference Result 31 states and 38 transitions.
[2025-04-28 21:21:39,462 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:39,463 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:39,463 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,464 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:39,465 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:39,465 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,466 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 1 mSDsluCounter, 48 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 78 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,470 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 78 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:39,471 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:39,477 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 27.
[2025-04-28 21:21:39,478 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 12 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:39,479 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:39,480 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:39,481 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,481 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:39,481 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:39,481 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:39,482 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:39,483 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,483 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,484 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:39,484 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,485 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,486 INFO  L85        PathProgramCache]: Analyzing trace with hash -2082010740, now seen corresponding path program 1 times
[2025-04-28 21:21:39,486 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,486 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1848203355]
[2025-04-28 21:21:39,486 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,487 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,503 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:39,543 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:39,544 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,545 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,204 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:40,206 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,207 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1848203355]
[2025-04-28 21:21:40,207 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1848203355] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,207 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [223995029]
[2025-04-28 21:21:40,207 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,207 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,211 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,216 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:40,218 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,325 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:40,366 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:40,367 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,367 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,370 INFO  L256         TraceCheckSpWp]: Trace formula consists of 113 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,377 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,837 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:40,838 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,302 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:43,302 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [223995029] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,302 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,302 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 12
[2025-04-28 21:21:43,303 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1180323544]
[2025-04-28 21:21:43,303 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,303 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:43,303 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,304 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:43,304 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=106, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:43,305 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 12 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 8 states have call predecessors, (16), 8 states have call successors, (16)
[2025-04-28 21:21:43,481 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,483 INFO  L93              Difference]: Finished difference Result 35 states and 47 transitions.
[2025-04-28 21:21:43,483 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:43,484 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 8 states have call predecessors, (16), 8 states have call successors, (16) Word has length 30
[2025-04-28 21:21:43,484 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,484 INFO  L225             Difference]: With dead ends: 35
[2025-04-28 21:21:43,484 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:21:43,485 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 70 GetRequests, 55 SyntacticMatches, 2 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 22 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=41, Invalid=169, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:43,486 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 4 mSDsluCounter, 183 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 210 SdHoareTripleChecker+Invalid, 82 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,487 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 210 Invalid, 82 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,489 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:21:43,497 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 33.
[2025-04-28 21:21:43,500 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 13 states have (on average 1.2307692307692308) internal successors, (16), 15 states have internal predecessors, (16), 10 states have call successors, (10), 6 states have call predecessors, (10), 9 states have return successors, (17), 12 states have call predecessors, (17), 10 states have call successors, (17)
[2025-04-28 21:21:43,501 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 43 transitions.
[2025-04-28 21:21:43,501 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 43 transitions. Word has length 30
[2025-04-28 21:21:43,501 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,501 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 43 transitions.
[2025-04-28 21:21:43,501 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 8 states have call predecessors, (16), 8 states have call successors, (16)
[2025-04-28 21:21:43,501 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 43 transitions.
[2025-04-28 21:21:43,502 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:43,502 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,502 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,507 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:43,706 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,707 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,707 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,707 INFO  L85        PathProgramCache]: Analyzing trace with hash 570309012, now seen corresponding path program 1 times
[2025-04-28 21:21:43,707 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,707 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [987084911]
[2025-04-28 21:21:43,708 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,708 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,719 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:43,726 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:43,726 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,727 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,772 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:43,772 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [987084911]
[2025-04-28 21:21:43,772 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [987084911] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1018336998]
[2025-04-28 21:21:43,772 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,773 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,775 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,777 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:43,781 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,828 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:43,846 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:43,846 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,846 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,847 INFO  L256         TraceCheckSpWp]: Trace formula consists of 113 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,848 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,868 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:43,868 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:43,868 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1018336998] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,869 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:43,869 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:43,869 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [38826846]
[2025-04-28 21:21:43,869 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,869 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,869 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,870 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,870 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,870 INFO  L87              Difference]: Start difference. First operand 33 states and 43 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:43,886 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,886 INFO  L93              Difference]: Finished difference Result 37 states and 49 transitions.
[2025-04-28 21:21:43,888 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:43,888 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:43,888 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,889 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:21:43,889 INFO  L226             Difference]: Without dead ends: 37
[2025-04-28 21:21:43,889 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,890 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 1 mSDsluCounter, 47 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 77 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,890 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 77 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:43,891 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 37 states.
[2025-04-28 21:21:43,898 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 37 to 37.
[2025-04-28 21:21:43,898 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 10 states have call successors, (10), 6 states have call predecessors, (10), 11 states have return successors, (21), 12 states have call predecessors, (21), 10 states have call successors, (21)
[2025-04-28 21:21:43,899 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 49 transitions.
[2025-04-28 21:21:43,899 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 49 transitions. Word has length 30
[2025-04-28 21:21:43,900 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,900 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 49 transitions.
[2025-04-28 21:21:43,900 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:43,900 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 49 transitions.
[2025-04-28 21:21:43,901 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:43,901 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,902 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,907 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:44,106 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,106 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,107 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,107 INFO  L85        PathProgramCache]: Analyzing trace with hash 1700736744, now seen corresponding path program 1 times
[2025-04-28 21:21:44,107 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,107 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [463313924]
[2025-04-28 21:21:44,107 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,107 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,117 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:44,123 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:44,123 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,123 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,179 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 18 proven. 1 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-04-28 21:21:44,180 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [463313924]
[2025-04-28 21:21:44,180 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [463313924] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1717079750]
[2025-04-28 21:21:44,180 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,180 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,183 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,185 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:44,188 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,252 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:44,285 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:44,285 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,285 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,286 INFO  L256         TraceCheckSpWp]: Trace formula consists of 185 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,288 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,303 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 20 proven. 1 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:44,304 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,559 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 18 proven. 1 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-04-28 21:21:44,559 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1717079750] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,559 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,559 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 4, 4] total 4
[2025-04-28 21:21:44,559 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [446455603]
[2025-04-28 21:21:44,560 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,560 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:44,560 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,561 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:44,561 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,561 INFO  L87              Difference]: Start difference. First operand 37 states and 49 transitions. Second operand  has 4 states, 3 states have (on average 5.666666666666667) internal successors, (17), 4 states have internal predecessors, (17), 3 states have call successors, (12), 2 states have call predecessors, (12), 3 states have return successors, (13), 3 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:44,578 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,578 INFO  L93              Difference]: Finished difference Result 37 states and 45 transitions.
[2025-04-28 21:21:44,579 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:44,580 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.666666666666667) internal successors, (17), 4 states have internal predecessors, (17), 3 states have call successors, (12), 2 states have call predecessors, (12), 3 states have return successors, (13), 3 states have call predecessors, (13), 3 states have call successors, (13) Word has length 45
[2025-04-28 21:21:44,580 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,580 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:21:44,581 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:44,581 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 93 GetRequests, 91 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,582 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 1 mSDsluCounter, 47 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 77 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,582 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 77 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:44,583 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:44,593 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:44,594 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 10 states have call successors, (10), 6 states have call predecessors, (10), 9 states have return successors, (17), 12 states have call predecessors, (17), 10 states have call successors, (17)
[2025-04-28 21:21:44,595 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 41 transitions.
[2025-04-28 21:21:44,595 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 41 transitions. Word has length 45
[2025-04-28 21:21:44,595 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,595 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 41 transitions.
[2025-04-28 21:21:44,595 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.666666666666667) internal successors, (17), 4 states have internal predecessors, (17), 3 states have call successors, (12), 2 states have call predecessors, (12), 3 states have return successors, (13), 3 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:44,596 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 41 transitions.
[2025-04-28 21:21:44,601 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:44,601 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,601 INFO  L218           NwaCegarLoop]: trace histogram [7, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,608 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:44,802 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,802 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,802 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,802 INFO  L85        PathProgramCache]: Analyzing trace with hash -498348184, now seen corresponding path program 2 times
[2025-04-28 21:21:44,803 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,803 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [258020084]
[2025-04-28 21:21:44,803 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:44,803 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,822 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:44,842 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:44,843 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:44,843 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,309 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 14 proven. 33 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:45,309 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,310 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [258020084]
[2025-04-28 21:21:45,310 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [258020084] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2063166477]
[2025-04-28 21:21:45,311 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,311 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,315 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,317 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,320 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,381 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:45,421 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:45,421 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,422 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,424 INFO  L256         TraceCheckSpWp]: Trace formula consists of 257 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,426 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,695 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 32 proven. 21 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:45,695 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,228 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 32 proven. 21 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:51,228 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2063166477] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,228 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,228 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 12] total 19
[2025-04-28 21:21:51,229 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [160882391]
[2025-04-28 21:21:51,229 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,230 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:51,230 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,231 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:51,232 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=286, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:51,233 INFO  L87              Difference]: Start difference. First operand 33 states and 41 transitions. Second operand  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 13 states have call successors, (23), 1 states have call predecessors, (23), 11 states have return successors, (29), 15 states have call predecessors, (29), 13 states have call successors, (29)
[2025-04-28 21:21:51,782 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,786 INFO  L93              Difference]: Finished difference Result 66 states and 105 transitions.
[2025-04-28 21:21:51,786 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:51,786 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 13 states have call successors, (23), 1 states have call predecessors, (23), 11 states have return successors, (29), 15 states have call predecessors, (29), 13 states have call successors, (29) Word has length 60
[2025-04-28 21:21:51,787 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,788 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:21:51,789 INFO  L226             Difference]: Without dead ends: 66
[2025-04-28 21:21:51,789 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 141 GetRequests, 108 SyntacticMatches, 5 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 175 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=160, Invalid=710, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:51,790 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 21 mSDsluCounter, 382 mSDsCounter, 0 mSdLazyCounter, 229 mSolverCounterSat, 64 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 422 SdHoareTripleChecker+Invalid, 293 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 64 IncrementalHoareTripleChecker+Valid, 229 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,790 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 422 Invalid, 293 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [64 Valid, 229 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:51,791 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-04-28 21:21:51,801 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 63.
[2025-04-28 21:21:51,801 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 25 states have (on average 1.12) internal successors, (28), 28 states have internal predecessors, (28), 20 states have call successors, (20), 10 states have call predecessors, (20), 17 states have return successors, (51), 24 states have call predecessors, (51), 20 states have call successors, (51)
[2025-04-28 21:21:51,805 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 99 transitions.
[2025-04-28 21:21:51,805 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 99 transitions. Word has length 60
[2025-04-28 21:21:51,806 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,806 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 99 transitions.
[2025-04-28 21:21:51,806 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 13 states have call successors, (23), 1 states have call predecessors, (23), 11 states have return successors, (29), 15 states have call predecessors, (29), 13 states have call successors, (29)
[2025-04-28 21:21:51,806 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 99 transitions.
[2025-04-28 21:21:51,810 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 181
[2025-04-28 21:21:51,810 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,810 INFO  L218           NwaCegarLoop]: trace histogram [23, 12, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,815 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,014 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,014 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,015 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,015 INFO  L85        PathProgramCache]: Analyzing trace with hash 954127208, now seen corresponding path program 3 times
[2025-04-28 21:21:52,015 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,015 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [651150321]
[2025-04-28 21:21:52,015 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,015 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,044 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 180 statements into 15 equivalence classes.
[2025-04-28 21:21:52,223 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 135 of 180 statements.
[2025-04-28 21:21:52,223 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:52,224 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,862 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 407 proven. 66 refuted. 0 times theorem prover too weak. 781 trivial. 0 not checked.
[2025-04-28 21:21:53,863 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,863 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [651150321]
[2025-04-28 21:21:53,863 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [651150321] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,863 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1830028441]
[2025-04-28 21:21:53,863 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:53,863 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,866 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,868 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,872 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,014 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 180 statements into 15 equivalence classes.
[2025-04-28 21:21:54,138 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 135 of 180 statements.
[2025-04-28 21:21:54,138 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:54,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,142 INFO  L256         TraceCheckSpWp]: Trace formula consists of 651 conjuncts, 38 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,152 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,617 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 446 proven. 63 refuted. 0 times theorem prover too weak. 745 trivial. 0 not checked.
[2025-04-28 21:21:54,617 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:05,830 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 405 proven. 71 refuted. 0 times theorem prover too weak. 778 trivial. 0 not checked.
[2025-04-28 21:22:05,830 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1830028441] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:05,830 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:05,830 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 15, 17] total 22
[2025-04-28 21:22:05,830 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [109727862]
[2025-04-28 21:22:05,830 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,831 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:05,831 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,832 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:05,832 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=71, Invalid=391, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:05,833 INFO  L87              Difference]: Start difference. First operand 63 states and 99 transitions. Second operand  has 22 states, 11 states have (on average 3.1818181818181817) internal successors, (35), 21 states have internal predecessors, (35), 18 states have call successors, (31), 2 states have call predecessors, (31), 11 states have return successors, (37), 16 states have call predecessors, (37), 18 states have call successors, (37)
[2025-04-28 21:22:06,167 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,167 INFO  L93              Difference]: Finished difference Result 87 states and 134 transitions.
[2025-04-28 21:22:06,167 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:06,168 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 3.1818181818181817) internal successors, (35), 21 states have internal predecessors, (35), 18 states have call successors, (31), 2 states have call predecessors, (31), 11 states have return successors, (37), 16 states have call predecessors, (37), 18 states have call successors, (37) Word has length 180
[2025-04-28 21:22:06,169 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,170 INFO  L225             Difference]: With dead ends: 87
[2025-04-28 21:22:06,170 INFO  L226             Difference]: Without dead ends: 87
[2025-04-28 21:22:06,171 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 383 GetRequests, 352 SyntacticMatches, 4 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 162 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=150, Invalid=662, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:22:06,171 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 17 mSDsluCounter, 223 mSDsCounter, 0 mSdLazyCounter, 186 mSolverCounterSat, 58 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 258 SdHoareTripleChecker+Invalid, 244 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 58 IncrementalHoareTripleChecker+Valid, 186 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,172 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 258 Invalid, 244 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [58 Valid, 186 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:06,172 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 87 states.
[2025-04-28 21:22:06,183 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 87 to 81.
[2025-04-28 21:22:06,183 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 33 states have (on average 1.0303030303030303) internal successors, (34), 32 states have internal predecessors, (34), 28 states have call successors, (28), 16 states have call predecessors, (28), 19 states have return successors, (61), 32 states have call predecessors, (61), 28 states have call successors, (61)
[2025-04-28 21:22:06,185 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 123 transitions.
[2025-04-28 21:22:06,185 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 123 transitions. Word has length 180
[2025-04-28 21:22:06,186 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,186 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 123 transitions.
[2025-04-28 21:22:06,186 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 3.1818181818181817) internal successors, (35), 21 states have internal predecessors, (35), 18 states have call successors, (31), 2 states have call predecessors, (31), 11 states have return successors, (37), 16 states have call predecessors, (37), 18 states have call successors, (37)
[2025-04-28 21:22:06,186 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 123 transitions.
[2025-04-28 21:22:06,188 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 151
[2025-04-28 21:22:06,189 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,189 INFO  L218           NwaCegarLoop]: trace histogram [19, 10, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,196 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:22:06,389 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,389 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,390 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,390 INFO  L85        PathProgramCache]: Analyzing trace with hash 1423672644, now seen corresponding path program 4 times
[2025-04-28 21:22:06,390 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,390 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1598227936]
[2025-04-28 21:22:06,390 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:06,390 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,409 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:22:06,441 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:22:06,441 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:06,441 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,334 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 80 proven. 199 refuted. 0 times theorem prover too weak. 558 trivial. 0 not checked.
[2025-04-28 21:22:07,334 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,334 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1598227936]
[2025-04-28 21:22:07,334 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1598227936] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,334 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [479895253]
[2025-04-28 21:22:07,334 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:07,334 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,337 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,339 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:07,342 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,557 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:22:07,657 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:22:07,657 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:07,657 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,659 INFO  L256         TraceCheckSpWp]: Trace formula consists of 689 conjuncts, 34 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,662 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,073 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 259 proven. 113 refuted. 0 times theorem prover too weak. 465 trivial. 0 not checked.
[2025-04-28 21:22:08,073 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
