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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:16,014 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:16,100 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ff13db3-1aa6-479b-90d4-33aefa23577e/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:16,110 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:16,110 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:16,143 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:16,144 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:16,144 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:16,146 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:16,146 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:16,147 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:16,147 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:16,148 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:16,148 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,148 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:16,148 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:16,149 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:16,149 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:16,149 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:16,149 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:16,150 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:16,467 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:16,479 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:16,482 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:16,484 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:16,484 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:16,487 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ff13db3-1aa6-479b-90d4-33aefa23577e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-024.smt2
[2025-04-28 21:21:16,490 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:16,494 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:16,704 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ff13db3-1aa6-479b-90d4-33aefa23577e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-024.smt2
[2025-04-28 21:21:16,712 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:16,713 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:16,714 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:16,714 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:16,714 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:16,721 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,757 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16 Unit
[2025-04-28 21:21:16,758 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:16,759 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:16,759 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:16,759 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:16,776 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,776 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,807 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,807 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,810 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,811 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,816 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,817 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,818 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,833 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:16,834 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:16,835 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:16,835 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:16,836 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,840 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,856 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,872 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:16,876 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:16,894 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:16,894 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:16,895 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:16,895 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:16,895 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:16,895 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:16,896 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo given in one single declaration
[2025-04-28 21:21:16,896 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo
[2025-04-28 21:21:16,896 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo
[2025-04-28 21:21:16,896 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo.AT.split given in one single declaration
[2025-04-28 21:21:16,896 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo.AT.split
[2025-04-28 21:21:16,897 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo.AT.split
[2025-04-28 21:21:16,897 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibo.AT_call given in one single declaration
[2025-04-28 21:21:16,897 INFO  L130     BoogieDeclarations]: Found specification of procedure fibo.AT_call
[2025-04-28 21:21:16,897 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibo.AT_call
[2025-04-28 21:21:16,897 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:16,897 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:16,897 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:16,897 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:16,897 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:16,897 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:16,953 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:16,955 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:17,118 INFO  L?                        ?]: Removed 18 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:17,119 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:17,133 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:17,134 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:17,134 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17 BoogieIcfgContainer
[2025-04-28 21:21:17,134 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:17,136 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:17,138 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:17,142 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:17,142 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:16" (1/3) ...
[2025-04-28 21:21:17,143 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@222e16a1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,144 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (2/3) ...
[2025-04-28 21:21:17,144 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@222e16a1 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,144 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17" (3/3) ...
[2025-04-28 21:21:17,145 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:17,161 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:17,163 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:17,205 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:17,218 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;@1a5a33e1, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:17,218 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:17,227 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:17,238 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:17,238 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,239 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:17,240 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,246 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,247 INFO  L85        PathProgramCache]: Analyzing trace with hash -628591717, now seen corresponding path program 1 times
[2025-04-28 21:21:17,256 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,256 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [873129107]
[2025-04-28 21:21:17,256 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,258 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,285 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:17,301 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:17,302 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,302 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,400 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:17,401 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,401 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [873129107]
[2025-04-28 21:21:17,402 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [873129107] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,402 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,409 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,411 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [301879859]
[2025-04-28 21:21:17,412 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,418 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,418 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,453 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,454 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,457 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:17,542 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,542 INFO  L93              Difference]: Finished difference Result 27 states and 32 transitions.
[2025-04-28 21:21:17,543 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,545 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:17,545 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,554 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:17,554 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:17,556 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:17,561 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.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,562 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.1s Time]
[2025-04-28 21:21:17,580 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:17,605 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:17,607 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:17,611 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:17,612 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:17,613 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,614 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:17,614 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:17,614 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:17,615 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:17,616 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,616 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:17,616 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:17,616 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,621 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,621 INFO  L85        PathProgramCache]: Analyzing trace with hash 2047682327, now seen corresponding path program 1 times
[2025-04-28 21:21:17,621 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,621 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [503293170]
[2025-04-28 21:21:17,621 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,622 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,633 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:17,642 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:17,642 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,643 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,732 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:17,733 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,733 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [503293170]
[2025-04-28 21:21:17,733 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [503293170] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,733 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,733 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,733 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [337759921]
[2025-04-28 21:21:17,733 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,735 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,735 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,740 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,740 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,741 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:17,801 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,802 INFO  L93              Difference]: Finished difference Result 31 states and 38 transitions.
[2025-04-28 21:21:17,802 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,802 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:17,803 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,803 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:17,804 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:17,804 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:17,805 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.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,808 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.1s Time]
[2025-04-28 21:21:17,810 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:17,822 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 27.
[2025-04-28 21:21:17,823 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:17,825 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:17,827 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:17,827 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,827 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:17,828 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:17,828 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:17,829 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:17,829 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,829 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:17,829 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:17,829 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,831 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,831 INFO  L85        PathProgramCache]: Analyzing trace with hash -98131277, now seen corresponding path program 1 times
[2025-04-28 21:21:17,833 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,833 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1144934716]
[2025-04-28 21:21:17,833 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,833 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,858 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:17,935 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:17,935 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,935 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,357 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:18,358 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,358 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1144934716]
[2025-04-28 21:21:18,358 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1144934716] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:18,358 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [943858743]
[2025-04-28 21:21:18,358 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,358 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,361 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:18,366 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:18,368 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:18,418 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:18,450 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:18,450 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,450 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,455 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,465 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:18,821 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:18,821 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:21,233 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:21,233 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [943858743] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:21,233 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:21,233 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 8
[2025-04-28 21:21:21,233 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1755746964]
[2025-04-28 21:21:21,234 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,234 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:21,234 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,238 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:21,238 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:21,238 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:21,335 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,336 INFO  L93              Difference]: Finished difference Result 34 states and 45 transitions.
[2025-04-28 21:21:21,338 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:21,338 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10) Word has length 30
[2025-04-28 21:21:21,338 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,339 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:21,339 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:21,339 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 57 SyntacticMatches, 3 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:21,340 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 3 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 117 SdHoareTripleChecker+Invalid, 38 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,341 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 117 Invalid, 38 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,343 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:21,349 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 32.
[2025-04-28 21:21:21,350 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 13 states have (on average 1.2307692307692308) internal successors, (16), 15 states have internal predecessors, (16), 9 states have call successors, (9), 6 states have call predecessors, (9), 9 states have return successors, (16), 11 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:21,352 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 41 transitions.
[2025-04-28 21:21:21,352 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 41 transitions. Word has length 30
[2025-04-28 21:21:21,352 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,352 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 41 transitions.
[2025-04-28 21:21:21,352 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (10), 1 states have call predecessors, (10), 5 states have return successors, (10), 6 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:21,353 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 41 transitions.
[2025-04-28 21:21:21,353 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:21,354 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,354 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:21,361 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:21,554 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:21,555 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,555 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,556 INFO  L85        PathProgramCache]: Analyzing trace with hash -1623937109, now seen corresponding path program 1 times
[2025-04-28 21:21:21,556 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,556 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2130761845]
[2025-04-28 21:21:21,556 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,556 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,566 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:21,581 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:21,581 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,581 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,648 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:21,649 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,649 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2130761845]
[2025-04-28 21:21:21,649 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2130761845] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:21,649 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1234373882]
[2025-04-28 21:21:21,649 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,649 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,652 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:21,655 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:21,678 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:21,734 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:21,758 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:21,758 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,758 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,760 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:21,761 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,793 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:21,795 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:21,795 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1234373882] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,795 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:21,795 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:21,796 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [105269841]
[2025-04-28 21:21:21,796 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,797 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:21,797 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,797 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:21,798 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:21,798 INFO  L87              Difference]: Start difference. First operand 32 states and 41 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 2 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 2 states have call successors, (8)
[2025-04-28 21:21:21,825 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,827 INFO  L93              Difference]: Finished difference Result 36 states and 45 transitions.
[2025-04-28 21:21:21,827 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:21,828 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 2 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 2 states have call successors, (8) Word has length 30
[2025-04-28 21:21:21,828 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,829 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:21,829 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:21,830 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:21,831 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, 2 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:21,833 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 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:21,835 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:21,842 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 36.
[2025-04-28 21:21:21,842 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 9 states have call successors, (9), 6 states have call predecessors, (9), 11 states have return successors, (18), 11 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:21,843 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 45 transitions.
[2025-04-28 21:21:21,846 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 45 transitions. Word has length 30
[2025-04-28 21:21:21,846 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,846 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 45 transitions.
[2025-04-28 21:21:21,846 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 2 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 2 states have call successors, (8)
[2025-04-28 21:21:21,846 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 45 transitions.
[2025-04-28 21:21:21,848 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:21,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,849 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:21,855 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:22,049 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:22,050 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,051 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,052 INFO  L85        PathProgramCache]: Analyzing trace with hash -389538591, now seen corresponding path program 1 times
[2025-04-28 21:21:22,052 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,052 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1634598207]
[2025-04-28 21:21:22,052 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,052 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,066 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:22,078 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:22,078 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,078 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,174 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 10 proven. 9 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-04-28 21:21:22,174 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1634598207]
[2025-04-28 21:21:22,174 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1634598207] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1205831368]
[2025-04-28 21:21:22,175 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,175 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,178 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,180 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:22,185 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,240 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:22,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:22,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,275 INFO  L256         TraceCheckSpWp]: Trace formula consists of 181 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,277 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:22,294 INFO  L134       CoverageAnalysis]: Checked inductivity of 39 backedges. 20 proven. 0 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:22,295 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:22,295 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1205831368] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:22,295 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:22,296 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:22,296 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [511077578]
[2025-04-28 21:21:22,296 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,296 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:22,296 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,297 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:22,297 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:22,297 INFO  L87              Difference]: Start difference. First operand 36 states and 45 transitions. Second operand  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:22,312 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,313 INFO  L93              Difference]: Finished difference Result 36 states and 43 transitions.
[2025-04-28 21:21:22,314 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:22,314 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11) Word has length 45
[2025-04-28 21:21:22,314 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,316 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:22,316 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:22,316 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 46 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:22,317 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:22,318 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:22,320 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:22,325 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:22,327 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 9 states have call successors, (9), 6 states have call predecessors, (9), 9 states have return successors, (16), 11 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:22,328 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 39 transitions.
[2025-04-28 21:21:22,328 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 39 transitions. Word has length 45
[2025-04-28 21:21:22,328 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,328 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 39 transitions.
[2025-04-28 21:21:22,331 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (11), 2 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:22,332 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 39 transitions.
[2025-04-28 21:21:22,333 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:22,333 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,333 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:22,340 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:22,533 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:22,534 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,534 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,534 INFO  L85        PathProgramCache]: Analyzing trace with hash 1904131543, now seen corresponding path program 2 times
[2025-04-28 21:21:22,534 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,534 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [463313924]
[2025-04-28 21:21:22,535 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:22,535 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,552 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:22,576 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:22,577 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:22,577 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,009 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 13 proven. 34 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:23,010 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [463313924]
[2025-04-28 21:21:23,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [463313924] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:23,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [285348485]
[2025-04-28 21:21:23,010 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:23,010 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:23,013 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:23,015 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:23,017 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:23,076 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:23,115 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:23,115 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:23,115 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,117 INFO  L256         TraceCheckSpWp]: Trace formula consists of 250 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:23,120 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,384 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 31 proven. 22 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:23,384 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,620 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 31 proven. 22 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:28,620 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [285348485] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,621 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,621 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 12] total 19
[2025-04-28 21:21:28,621 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2042159006]
[2025-04-28 21:21:28,621 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,622 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:28,622 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,622 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:28,623 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=286, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:28,623 INFO  L87              Difference]: Start difference. First operand 32 states and 39 transitions. Second operand  has 19 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 17 states have internal predecessors, (27), 12 states have call successors, (24), 1 states have call predecessors, (24), 11 states have return successors, (30), 18 states have call predecessors, (30), 12 states have call successors, (30)
[2025-04-28 21:21:29,194 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,195 INFO  L93              Difference]: Finished difference Result 63 states and 99 transitions.
[2025-04-28 21:21:29,195 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:29,195 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), 12 states have call successors, (24), 1 states have call predecessors, (24), 11 states have return successors, (30), 18 states have call predecessors, (30), 12 states have call successors, (30) Word has length 60
[2025-04-28 21:21:29,196 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,197 INFO  L225             Difference]: With dead ends: 63
[2025-04-28 21:21:29,197 INFO  L226             Difference]: Without dead ends: 63
[2025-04-28 21:21:29,200 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 141 GetRequests, 108 SyntacticMatches, 5 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 175 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=160, Invalid=710, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:29,201 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 24 mSDsluCounter, 348 mSDsCounter, 0 mSdLazyCounter, 262 mSolverCounterSat, 66 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 390 SdHoareTripleChecker+Invalid, 328 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 66 IncrementalHoareTripleChecker+Valid, 262 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,201 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 390 Invalid, 328 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [66 Valid, 262 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:29,201 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 63 states.
[2025-04-28 21:21:29,216 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 63 to 61.
[2025-04-28 21:21:29,216 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 61 states, 25 states have (on average 1.12) internal successors, (28), 28 states have internal predecessors, (28), 18 states have call successors, (18), 10 states have call predecessors, (18), 17 states have return successors, (49), 22 states have call predecessors, (49), 18 states have call successors, (49)
[2025-04-28 21:21:29,218 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 61 states to 61 states and 95 transitions.
[2025-04-28 21:21:29,218 INFO  L79                 Accepts]: Start accepts. Automaton has 61 states and 95 transitions. Word has length 60
[2025-04-28 21:21:29,218 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,218 INFO  L485      AbstractCegarLoop]: Abstraction has 61 states and 95 transitions.
[2025-04-28 21:21:29,219 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), 12 states have call successors, (24), 1 states have call predecessors, (24), 11 states have return successors, (30), 18 states have call predecessors, (30), 12 states have call successors, (30)
[2025-04-28 21:21:29,219 INFO  L278                IsEmpty]: Start isEmpty. Operand 61 states and 95 transitions.
[2025-04-28 21:21:29,224 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 181
[2025-04-28 21:21:29,224 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,224 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:29,231 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:29,425 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:29,425 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,426 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,426 INFO  L85        PathProgramCache]: Analyzing trace with hash -140229545, now seen corresponding path program 3 times
[2025-04-28 21:21:29,426 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,426 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1644866011]
[2025-04-28 21:21:29,426 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:29,426 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,450 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 180 statements into 14 equivalence classes.
[2025-04-28 21:21:29,533 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s) and asserted 131 of 180 statements.
[2025-04-28 21:21:29,533 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s)
[2025-04-28 21:21:29,533 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,913 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 394 proven. 74 refuted. 0 times theorem prover too weak. 786 trivial. 0 not checked.
[2025-04-28 21:21:30,913 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1644866011]
[2025-04-28 21:21:30,913 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1644866011] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [140439989]
[2025-04-28 21:21:30,913 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:30,913 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,917 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,919 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:30,926 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,052 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 180 statements into 14 equivalence classes.
[2025-04-28 21:21:31,164 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s) and asserted 131 of 180 statements.
[2025-04-28 21:21:31,164 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s)
[2025-04-28 21:21:31,164 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,167 INFO  L256         TraceCheckSpWp]: Trace formula consists of 581 conjuncts, 41 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,177 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,646 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 393 proven. 72 refuted. 0 times theorem prover too weak. 789 trivial. 0 not checked.
[2025-04-28 21:21:31,649 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,390 INFO  L134       CoverageAnalysis]: Checked inductivity of 1254 backedges. 391 proven. 80 refuted. 0 times theorem prover too weak. 783 trivial. 0 not checked.
[2025-04-28 21:21:42,390 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [140439989] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,390 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,391 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 14, 17] total 22
[2025-04-28 21:21:42,391 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1865857049]
[2025-04-28 21:21:42,391 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,392 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:42,392 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,393 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:42,393 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=71, Invalid=391, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:42,393 INFO  L87              Difference]: Start difference. First operand 61 states and 95 transitions. Second operand  has 22 states, 11 states have (on average 3.090909090909091) internal successors, (34), 21 states have internal predecessors, (34), 13 states have call successors, (33), 1 states have call predecessors, (33), 11 states have return successors, (40), 19 states have call predecessors, (40), 13 states have call successors, (40)
[2025-04-28 21:21:42,695 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,695 INFO  L93              Difference]: Finished difference Result 83 states and 126 transitions.
[2025-04-28 21:21:42,696 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:42,696 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 3.090909090909091) internal successors, (34), 21 states have internal predecessors, (34), 13 states have call successors, (33), 1 states have call predecessors, (33), 11 states have return successors, (40), 19 states have call predecessors, (40), 13 states have call successors, (40) Word has length 180
[2025-04-28 21:21:42,697 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,699 INFO  L225             Difference]: With dead ends: 83
[2025-04-28 21:21:42,699 INFO  L226             Difference]: Without dead ends: 83
[2025-04-28 21:21:42,700 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 383 GetRequests, 351 SyntacticMatches, 5 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 163 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=150, Invalid=662, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:42,700 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 15 mSDsluCounter, 265 mSDsCounter, 0 mSdLazyCounter, 197 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 298 SdHoareTripleChecker+Invalid, 238 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 197 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,700 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 298 Invalid, 238 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 197 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:42,701 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 83 states.
[2025-04-28 21:21:42,714 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 83 to 79.
[2025-04-28 21:21:42,714 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 33 states have (on average 1.0303030303030303) internal successors, (34), 32 states have internal predecessors, (34), 26 states have call successors, (26), 16 states have call predecessors, (26), 19 states have return successors, (59), 30 states have call predecessors, (59), 26 states have call successors, (59)
[2025-04-28 21:21:42,716 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 119 transitions.
[2025-04-28 21:21:42,716 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 119 transitions. Word has length 180
[2025-04-28 21:21:42,717 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,717 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 119 transitions.
[2025-04-28 21:21:42,717 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 3.090909090909091) internal successors, (34), 21 states have internal predecessors, (34), 13 states have call successors, (33), 1 states have call predecessors, (33), 11 states have return successors, (40), 19 states have call predecessors, (40), 13 states have call successors, (40)
[2025-04-28 21:21:42,717 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 119 transitions.
[2025-04-28 21:21:42,720 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 151
[2025-04-28 21:21:42,720 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,720 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:21:42,725 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:42,925 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:21:42,926 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,926 INFO  L85        PathProgramCache]: Analyzing trace with hash -419005189, now seen corresponding path program 4 times
[2025-04-28 21:21:42,926 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,926 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1212589834]
[2025-04-28 21:21:42,927 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:42,927 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,970 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:21:43,024 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:21:43,024 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:43,024 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,966 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 247 proven. 118 refuted. 0 times theorem prover too weak. 472 trivial. 0 not checked.
[2025-04-28 21:21:43,967 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1212589834]
[2025-04-28 21:21:43,967 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1212589834] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,967 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [631911731]
[2025-04-28 21:21:43,967 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:43,967 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,970 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,972 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,974 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,161 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 150 statements into 2 equivalence classes.
[2025-04-28 21:21:44,256 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 150 of 150 statements.
[2025-04-28 21:21:44,256 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:44,256 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,259 INFO  L256         TraceCheckSpWp]: Trace formula consists of 664 conjuncts, 27 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,264 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,553 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 247 proven. 118 refuted. 0 times theorem prover too weak. 472 trivial. 0 not checked.
[2025-04-28 21:21:44,554 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
