./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-119.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:46,807 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:46,886 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4f0acccd-267e-46f0-93af-0f74c082a9e0/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:46,894 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:46,894 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:46,925 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:46,926 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:46,927 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:46,928 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:46,928 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:46,929 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:46,929 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:46,930 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:46,930 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:46,930 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:46,931 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:46,931 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:46,931 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:46,931 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:46,931 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:46,931 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:46,932 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:46,932 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:46,932 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:46,932 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:46,933 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:46,933 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:47,255 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:47,267 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:47,271 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:47,274 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:47,275 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:47,276 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4f0acccd-267e-46f0-93af-0f74c082a9e0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-119.smt2
[2025-04-28 21:21:47,278 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:47,282 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:47,753 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4f0acccd-267e-46f0-93af-0f74c082a9e0/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-119.smt2
[2025-04-28 21:21:47,758 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:47,762 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:47,764 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:47,764 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:47,764 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:47,767 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,816 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47 Unit
[2025-04-28 21:21:47,817 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:47,818 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:47,818 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:47,818 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:47,835 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,836 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,880 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,884 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,894 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,896 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,898 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,901 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,903 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,938 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:47,939 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:47,942 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:47,942 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:47,943 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (1/1) ...
[2025-04-28 21:21:47,946 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:47,970 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,985 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:47,988 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:47,999 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:48,000 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:48,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:48,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:48,000 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:48,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:48,000 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcmainStart__sem given in one single declaration
[2025-04-28 21:21:48,000 INFO  L130     BoogieDeclarations]: Found specification of procedure funcmainStart__sem
[2025-04-28 21:21:48,000 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcmainStart__sem
[2025-04-28 21:21:48,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:48,001 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:48,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:48,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT1__sem given in one single declaration
[2025-04-28 21:21:48,001 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT1__sem
[2025-04-28 21:21:48,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT1__sem
[2025-04-28 21:21:48,001 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT4__sem given in one single declaration
[2025-04-28 21:21:48,001 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT4__sem
[2025-04-28 21:21:48,001 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT4__sem
[2025-04-28 21:21:48,002 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcNT3__sem given in one single declaration
[2025-04-28 21:21:48,002 INFO  L130     BoogieDeclarations]: Found specification of procedure funcNT3__sem
[2025-04-28 21:21:48,002 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcNT3__sem
[2025-04-28 21:21:48,002 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:48,002 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:48,002 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:48,184 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:48,187 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:48,657 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:48,657 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:48,670 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:48,670 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:48,671 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:48 BoogieIcfgContainer
[2025-04-28 21:21:48,671 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:48,673 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:48,675 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:48,678 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:48,679 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:47" (1/3) ...
[2025-04-28 21:21:48,680 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@47cf142c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:48, skipping insertion in model container
[2025-04-28 21:21:48,680 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:47" (2/3) ...
[2025-04-28 21:21:48,680 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@47cf142c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:48, skipping insertion in model container
[2025-04-28 21:21:48,680 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:48" (3/3) ...
[2025-04-28 21:21:48,682 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:48,698 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:48,701 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 42 locations, 79 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:48,756 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:48,778 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;@2b0c73f2, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:48,778 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:48,783 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 42 states, 15 states have (on average 1.6666666666666667) internal successors, (25), 21 states have internal predecessors, (25), 18 states have call successors, (18), 7 states have call predecessors, (18), 7 states have return successors, (18), 14 states have call predecessors, (18), 18 states have call successors, (18)
[2025-04-28 21:21:48,829 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:48,829 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,830 INFO  L218           NwaCegarLoop]: trace histogram [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:48,830 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,840 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,841 INFO  L85        PathProgramCache]: Analyzing trace with hash -2011215310, now seen corresponding path program 1 times
[2025-04-28 21:21:48,849 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,849 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1845278283]
[2025-04-28 21:21:48,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,850 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,918 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:49,134 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:49,135 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,135 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,988 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:49,990 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,991 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1845278283]
[2025-04-28 21:21:49,992 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1845278283] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,992 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,997 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:49,999 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [16829499]
[2025-04-28 21:21:50,000 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,007 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:50,007 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,044 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:50,045 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:50,048 INFO  L87              Difference]: Start difference. First operand  has 42 states, 15 states have (on average 1.6666666666666667) internal successors, (25), 21 states have internal predecessors, (25), 18 states have call successors, (18), 7 states have call predecessors, (18), 7 states have return successors, (18), 14 states have call predecessors, (18), 18 states have call successors, (18) Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:50,426 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,427 INFO  L93              Difference]: Finished difference Result 46 states and 71 transitions.
[2025-04-28 21:21:50,430 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:50,431 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:50,432 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,445 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:50,445 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:50,447 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:50,454 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 3 mSDsluCounter, 224 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 273 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,454 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 273 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:50,468 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:50,491 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-04-28 21:21:50,495 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 15 states have (on average 1.6) internal successors, (24), 21 states have internal predecessors, (24), 18 states have call successors, (18), 7 states have call predecessors, (18), 8 states have return successors, (25), 14 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:21:50,503 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 67 transitions.
[2025-04-28 21:21:50,505 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 67 transitions. Word has length 20
[2025-04-28 21:21:50,506 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,506 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 67 transitions.
[2025-04-28 21:21:50,506 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:50,506 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 67 transitions.
[2025-04-28 21:21:50,508 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:50,509 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,509 INFO  L218           NwaCegarLoop]: trace histogram [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:50,510 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:50,510 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,511 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,511 INFO  L85        PathProgramCache]: Analyzing trace with hash -1494884434, now seen corresponding path program 1 times
[2025-04-28 21:21:50,511 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,511 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [323707210]
[2025-04-28 21:21:50,511 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,511 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,540 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:50,596 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:50,598 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,598 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,900 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:50,900 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,900 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [323707210]
[2025-04-28 21:21:50,900 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [323707210] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,900 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,900 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:50,900 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1195626510]
[2025-04-28 21:21:50,900 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,901 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:50,902 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,902 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:50,902 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:50,902 INFO  L87              Difference]: Start difference. First operand 42 states and 67 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,153 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,153 INFO  L93              Difference]: Finished difference Result 48 states and 79 transitions.
[2025-04-28 21:21:51,154 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:51,154 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:51,155 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,158 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:51,158 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:51,158 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:51,159 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 3 mSDsluCounter, 263 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 320 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,159 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 320 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,160 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:51,174 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:21:51,175 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 15 states have (on average 1.6) internal successors, (24), 21 states have internal predecessors, (24), 18 states have call successors, (18), 7 states have call predecessors, (18), 8 states have return successors, (25), 14 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:21:51,176 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 67 transitions.
[2025-04-28 21:21:51,176 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 67 transitions. Word has length 20
[2025-04-28 21:21:51,177 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,177 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 67 transitions.
[2025-04-28 21:21:51,177 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,177 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 67 transitions.
[2025-04-28 21:21:51,178 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:51,178 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,178 INFO  L218           NwaCegarLoop]: trace histogram [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:51,179 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:51,179 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,179 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,179 INFO  L85        PathProgramCache]: Analyzing trace with hash 992924796, now seen corresponding path program 1 times
[2025-04-28 21:21:51,180 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,180 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1734970029]
[2025-04-28 21:21:51,180 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,180 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,200 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:51,234 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:51,234 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,234 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,549 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:51,549 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,549 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1734970029]
[2025-04-28 21:21:51,549 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1734970029] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,550 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,550 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:51,550 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1016798328]
[2025-04-28 21:21:51,550 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,550 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:51,550 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,551 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:51,551 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:51,551 INFO  L87              Difference]: Start difference. First operand 42 states and 67 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,810 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,810 INFO  L93              Difference]: Finished difference Result 48 states and 79 transitions.
[2025-04-28 21:21:51,811 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:51,811 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:51,811 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,812 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:51,813 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:51,813 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:51,813 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 3 mSDsluCounter, 263 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 320 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,814 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 320 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,815 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:51,825 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:21:51,826 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 15 states have (on average 1.6) internal successors, (24), 21 states have internal predecessors, (24), 18 states have call successors, (18), 7 states have call predecessors, (18), 8 states have return successors, (25), 14 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:21:51,828 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 67 transitions.
[2025-04-28 21:21:51,830 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 67 transitions. Word has length 20
[2025-04-28 21:21:51,830 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,830 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 67 transitions.
[2025-04-28 21:21:51,830 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,831 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 67 transitions.
[2025-04-28 21:21:51,831 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:51,832 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,832 INFO  L218           NwaCegarLoop]: trace histogram [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:51,832 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:51,832 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,832 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,832 INFO  L85        PathProgramCache]: Analyzing trace with hash -978553558, now seen corresponding path program 1 times
[2025-04-28 21:21:51,833 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,833 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [731170889]
[2025-04-28 21:21:51,833 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,833 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,849 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:51,884 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:51,884 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,884 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,131 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:52,132 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,132 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [731170889]
[2025-04-28 21:21:52,132 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [731170889] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,132 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,132 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:52,133 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1170408780]
[2025-04-28 21:21:52,133 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,133 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:52,133 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,134 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:52,134 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:52,135 INFO  L87              Difference]: Start difference. First operand 42 states and 67 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,395 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,395 INFO  L93              Difference]: Finished difference Result 48 states and 79 transitions.
[2025-04-28 21:21:52,395 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:52,396 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:52,396 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,397 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:52,397 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:52,397 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:52,398 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 3 mSDsluCounter, 263 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 320 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,398 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 320 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,400 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:52,406 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:21:52,406 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 15 states have (on average 1.6) internal successors, (24), 21 states have internal predecessors, (24), 18 states have call successors, (18), 7 states have call predecessors, (18), 8 states have return successors, (25), 14 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:21:52,407 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 67 transitions.
[2025-04-28 21:21:52,407 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 67 transitions. Word has length 20
[2025-04-28 21:21:52,407 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,407 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 67 transitions.
[2025-04-28 21:21:52,407 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,407 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 67 transitions.
[2025-04-28 21:21:52,408 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:52,409 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,409 INFO  L218           NwaCegarLoop]: trace histogram [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:52,409 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:52,409 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,409 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,409 INFO  L85        PathProgramCache]: Analyzing trace with hash -720388120, now seen corresponding path program 1 times
[2025-04-28 21:21:52,410 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,410 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [139653327]
[2025-04-28 21:21:52,410 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,410 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,426 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:52,472 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:52,473 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,473 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,701 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:52,701 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,701 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [139653327]
[2025-04-28 21:21:52,701 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [139653327] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,701 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,701 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:52,701 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2086277031]
[2025-04-28 21:21:52,701 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,702 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:52,702 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,702 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:52,702 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:52,703 INFO  L87              Difference]: Start difference. First operand 42 states and 67 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,915 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,916 INFO  L93              Difference]: Finished difference Result 48 states and 79 transitions.
[2025-04-28 21:21:52,916 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:52,916 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:52,917 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,918 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:52,918 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:52,918 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:52,919 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 3 mSDsluCounter, 263 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 320 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,919 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 320 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,920 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:52,925 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:21:52,925 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 15 states have (on average 1.6) internal successors, (24), 20 states have internal predecessors, (24), 18 states have call successors, (18), 7 states have call predecessors, (18), 8 states have return successors, (25), 14 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:21:52,926 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 67 transitions.
[2025-04-28 21:21:52,926 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 67 transitions. Word has length 20
[2025-04-28 21:21:52,926 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,926 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 67 transitions.
[2025-04-28 21:21:52,926 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,926 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 67 transitions.
[2025-04-28 21:21:52,927 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:52,928 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,928 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]
[2025-04-28 21:21:52,928 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:52,928 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,928 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,928 INFO  L85        PathProgramCache]: Analyzing trace with hash 365406542, now seen corresponding path program 1 times
[2025-04-28 21:21:52,928 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,928 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1804435289]
[2025-04-28 21:21:52,929 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,929 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,951 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:52,987 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:52,987 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,987 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,565 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:53,565 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,565 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1804435289]
[2025-04-28 21:21:53,565 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1804435289] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,565 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1344079238]
[2025-04-28 21:21:53,565 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,565 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,570 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,575 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:53,579 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,753 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:53,929 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:53,929 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,929 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,942 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,950 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,169 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:54,169 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,572 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:56,572 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1344079238] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,572 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,572 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 15
[2025-04-28 21:21:56,573 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [668526996]
[2025-04-28 21:21:56,573 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,573 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:56,573 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,574 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:56,574 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=173, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:56,574 INFO  L87              Difference]: Start difference. First operand 42 states and 67 transitions. Second operand  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:57,200 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,200 INFO  L93              Difference]: Finished difference Result 53 states and 102 transitions.
[2025-04-28 21:21:57,201 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:57,201 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13) Word has length 28
[2025-04-28 21:21:57,202 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,203 INFO  L225             Difference]: With dead ends: 53
[2025-04-28 21:21:57,203 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:57,203 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 49 SyntacticMatches, 4 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 27 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=56, Invalid=250, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:57,204 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 8 mSDsluCounter, 344 mSDsCounter, 0 mSdLazyCounter, 317 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 398 SdHoareTripleChecker+Invalid, 324 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 317 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,205 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 398 Invalid, 324 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 317 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:57,205 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:57,214 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 45.
[2025-04-28 21:21:57,214 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 16 states have (on average 1.5625) internal successors, (25), 22 states have internal predecessors, (25), 19 states have call successors, (19), 7 states have call predecessors, (19), 9 states have return successors, (35), 16 states have call predecessors, (35), 19 states have call successors, (35)
[2025-04-28 21:21:57,215 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 79 transitions.
[2025-04-28 21:21:57,215 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 79 transitions. Word has length 28
[2025-04-28 21:21:57,217 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,217 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 79 transitions.
[2025-04-28 21:21:57,217 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:57,217 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 79 transitions.
[2025-04-28 21:21:57,219 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:57,219 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,219 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:57,228 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:57,419 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable6
[2025-04-28 21:21:57,420 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,420 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,420 INFO  L85        PathProgramCache]: Analyzing trace with hash -1656827958, now seen corresponding path program 1 times
[2025-04-28 21:21:57,420 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,420 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1157557978]
[2025-04-28 21:21:57,420 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,421 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,444 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:57,485 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:57,485 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,485 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,868 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:57,868 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,868 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1157557978]
[2025-04-28 21:21:57,868 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1157557978] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,868 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1154796092]
[2025-04-28 21:21:57,868 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,868 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,871 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,873 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:57,877 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,026 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:58,184 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:58,184 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,184 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,195 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,198 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,304 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:58,304 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:00,029 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,029 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1154796092] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,029 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,030 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 10, 10] total 15
[2025-04-28 21:22:00,030 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [991078618]
[2025-04-28 21:22:00,030 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,031 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:22:00,033 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,033 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:22:00,034 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=171, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:22:00,034 INFO  L87              Difference]: Start difference. First operand 45 states and 79 transitions. Second operand  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:22:00,754 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,755 INFO  L93              Difference]: Finished difference Result 58 states and 128 transitions.
[2025-04-28 21:22:00,755 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:00,756 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12) Word has length 28
[2025-04-28 21:22:00,756 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,757 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:22:00,757 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:22:00,758 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 49 SyntacticMatches, 4 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 29 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=58, Invalid=248, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:22:00,762 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 8 mSDsluCounter, 288 mSDsCounter, 0 mSdLazyCounter, 347 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 344 SdHoareTripleChecker+Invalid, 362 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 347 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,762 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 344 Invalid, 362 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 347 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:22:00,763 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:22:00,785 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 50.
[2025-04-28 21:22:00,785 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 18 states have (on average 1.5) internal successors, (27), 25 states have internal predecessors, (27), 20 states have call successors, (20), 7 states have call predecessors, (20), 11 states have return successors, (56), 18 states have call predecessors, (56), 20 states have call successors, (56)
[2025-04-28 21:22:00,786 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 103 transitions.
[2025-04-28 21:22:00,786 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 103 transitions. Word has length 28
[2025-04-28 21:22:00,786 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,787 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 103 transitions.
[2025-04-28 21:22:00,787 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:22:00,787 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 103 transitions.
[2025-04-28 21:22:00,788 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:00,788 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,788 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:22:00,797 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:22:00,989 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,989 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,989 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,990 INFO  L85        PathProgramCache]: Analyzing trace with hash 1126025496, now seen corresponding path program 1 times
[2025-04-28 21:22:00,990 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,990 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [739191509]
[2025-04-28 21:22:00,990 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,990 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,005 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:01,050 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:01,050 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,051 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:01,464 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,464 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [739191509]
[2025-04-28 21:22:01,464 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [739191509] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1487389838]
[2025-04-28 21:22:01,465 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,465 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,467 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,469 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:22:01,473 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,650 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:01,767 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:01,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,768 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,771 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,773 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,029 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:02,029 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:04,107 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:04,107 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1487389838] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:04,107 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:04,108 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:22:04,108 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [370403120]
[2025-04-28 21:22:04,108 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,108 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:04,108 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,109 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:04,109 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=498, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:04,110 INFO  L87              Difference]: Start difference. First operand 50 states and 103 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:05,252 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,252 INFO  L93              Difference]: Finished difference Result 64 states and 158 transitions.
[2025-04-28 21:22:05,253 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:05,253 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:22:05,253 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,254 INFO  L225             Difference]: With dead ends: 64
[2025-04-28 21:22:05,255 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:22:05,255 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=110, Invalid=946, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:05,256 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 14 mSDsluCounter, 759 mSDsCounter, 0 mSdLazyCounter, 756 mSolverCounterSat, 43 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 814 SdHoareTripleChecker+Invalid, 799 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 43 IncrementalHoareTripleChecker+Valid, 756 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,256 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 814 Invalid, 799 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [43 Valid, 756 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:05,257 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:22:05,270 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 52.
[2025-04-28 21:22:05,270 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 19 states have (on average 1.4736842105263157) internal successors, (28), 27 states have internal predecessors, (28), 20 states have call successors, (20), 7 states have call predecessors, (20), 12 states have return successors, (65), 18 states have call predecessors, (65), 20 states have call successors, (65)
[2025-04-28 21:22:05,271 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 113 transitions.
[2025-04-28 21:22:05,272 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 113 transitions. Word has length 28
[2025-04-28 21:22:05,272 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,272 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 113 transitions.
[2025-04-28 21:22:05,272 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:05,272 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 113 transitions.
[2025-04-28 21:22:05,273 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:05,273 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,274 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:22:05,280 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:05,474 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,474 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,474 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,475 INFO  L85        PathProgramCache]: Analyzing trace with hash 615904838, now seen corresponding path program 1 times
[2025-04-28 21:22:05,475 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,475 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [73917937]
[2025-04-28 21:22:05,475 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,475 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,488 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:05,522 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:05,522 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:05,522 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,902 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:05,902 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:05,902 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [73917937]
[2025-04-28 21:22:05,902 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [73917937] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:05,902 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2011765660]
[2025-04-28 21:22:05,902 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,903 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,905 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:05,907 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:05,910 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,091 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:06,216 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:06,216 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,217 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,224 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,230 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:06,458 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,458 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,543 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:08,543 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2011765660] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,543 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,543 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:22:08,544 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1557997712]
[2025-04-28 21:22:08,544 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,544 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:08,544 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,545 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:08,545 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=498, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:08,545 INFO  L87              Difference]: Start difference. First operand 52 states and 113 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:09,674 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,674 INFO  L93              Difference]: Finished difference Result 66 states and 168 transitions.
[2025-04-28 21:22:09,675 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:09,675 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:22:09,675 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,677 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:22:09,677 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:22:09,677 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=110, Invalid=946, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:09,678 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 15 mSDsluCounter, 720 mSDsCounter, 0 mSdLazyCounter, 716 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 775 SdHoareTripleChecker+Invalid, 763 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 716 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,678 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 775 Invalid, 763 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 716 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:09,679 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:22:09,692 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 52.
[2025-04-28 21:22:09,693 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 19 states have (on average 1.4736842105263157) internal successors, (28), 27 states have internal predecessors, (28), 20 states have call successors, (20), 7 states have call predecessors, (20), 12 states have return successors, (65), 18 states have call predecessors, (65), 20 states have call successors, (65)
[2025-04-28 21:22:09,694 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 113 transitions.
[2025-04-28 21:22:09,694 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 113 transitions. Word has length 28
[2025-04-28 21:22:09,694 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,694 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 113 transitions.
[2025-04-28 21:22:09,695 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:09,695 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 113 transitions.
[2025-04-28 21:22:09,696 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:09,696 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,696 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:22:09,703 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:22:09,900 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:09,900 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,901 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,901 INFO  L85        PathProgramCache]: Analyzing trace with hash -395212412, now seen corresponding path program 1 times
[2025-04-28 21:22:09,901 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,901 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [252721935]
[2025-04-28 21:22:09,901 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,901 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,931 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:10,002 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:10,002 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,002 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,327 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:10,327 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:10,327 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [252721935]
[2025-04-28 21:22:10,328 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [252721935] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:10,328 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [218091715]
[2025-04-28 21:22:10,328 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:10,328 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:10,331 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:10,333 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:10,337 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:22:10,536 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:10,659 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:10,659 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,660 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,663 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:10,664 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,862 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:22:10,863 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:12,342 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:22:12,342 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [218091715] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:12,343 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:12,343 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 24
[2025-04-28 21:22:12,343 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [536563856]
[2025-04-28 21:22:12,343 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,343 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:12,343 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,344 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:12,344 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=55, Invalid=497, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:12,344 INFO  L87              Difference]: Start difference. First operand 52 states and 113 transitions. Second operand  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:13,609 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,609 INFO  L93              Difference]: Finished difference Result 65 states and 169 transitions.
[2025-04-28 21:22:13,609 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:13,609 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:22:13,610 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,611 INFO  L225             Difference]: With dead ends: 65
[2025-04-28 21:22:13,611 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:22:13,611 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 75 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 63 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=112, Invalid=944, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:13,612 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 9 mSDsluCounter, 901 mSDsCounter, 0 mSdLazyCounter, 1046 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 957 SdHoareTripleChecker+Invalid, 1068 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 1046 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,612 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 957 Invalid, 1068 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 1046 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:22:13,613 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:22:13,628 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 57.
[2025-04-28 21:22:13,629 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 21 states have (on average 1.4285714285714286) internal successors, (30), 29 states have internal predecessors, (30), 21 states have call successors, (21), 7 states have call predecessors, (21), 14 states have return successors, (91), 20 states have call predecessors, (91), 21 states have call successors, (91)
[2025-04-28 21:22:13,630 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 142 transitions.
[2025-04-28 21:22:13,630 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 142 transitions. Word has length 28
[2025-04-28 21:22:13,630 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,630 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 142 transitions.
[2025-04-28 21:22:13,630 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.25) internal successors, (27), 21 states have internal predecessors, (27), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:13,630 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 142 transitions.
[2025-04-28 21:22:13,632 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:13,632 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,632 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:22:13,644 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:22:13,832 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,833 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,833 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,833 INFO  L85        PathProgramCache]: Analyzing trace with hash 672084426, now seen corresponding path program 2 times
[2025-04-28 21:22:13,833 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,833 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2067083557]
[2025-04-28 21:22:13,833 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:13,834 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,848 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:22:13,879 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:13,880 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:13,880 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,206 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:14,206 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:14,206 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2067083557]
[2025-04-28 21:22:14,206 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2067083557] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:14,206 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2046469127]
[2025-04-28 21:22:14,206 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:14,206 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:14,209 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:14,211 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:14,215 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:14,429 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:22:14,554 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:14,554 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:14,554 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,559 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:14,563 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:14,738 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:14,738 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:16,157 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:16,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2046469127] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:16,157 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:16,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 10, 10] total 23
[2025-04-28 21:22:16,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1261542275]
[2025-04-28 21:22:16,157 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:16,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:22:16,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:16,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:22:16,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=453, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:22:16,159 INFO  L87              Difference]: Start difference. First operand 57 states and 142 transitions. Second operand  has 23 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 20 states have internal predecessors, (26), 13 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:17,219 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:17,219 INFO  L93              Difference]: Finished difference Result 68 states and 193 transitions.
[2025-04-28 21:22:17,220 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:22:17,220 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 20 states have internal predecessors, (26), 13 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:22:17,220 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:17,222 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:22:17,222 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:22:17,222 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 76 GetRequests, 41 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 72 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=125, Invalid=931, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:17,223 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 16 mSDsluCounter, 715 mSDsCounter, 0 mSdLazyCounter, 772 mSolverCounterSat, 47 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 768 SdHoareTripleChecker+Invalid, 819 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 47 IncrementalHoareTripleChecker+Valid, 772 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:17,223 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 768 Invalid, 819 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [47 Valid, 772 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:17,224 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:22:17,246 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 62.
[2025-04-28 21:22:17,246 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 23 states have (on average 1.391304347826087) internal successors, (32), 31 states have internal predecessors, (32), 22 states have call successors, (22), 7 states have call predecessors, (22), 16 states have return successors, (122), 23 states have call predecessors, (122), 22 states have call successors, (122)
[2025-04-28 21:22:17,248 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 176 transitions.
[2025-04-28 21:22:17,248 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 176 transitions. Word has length 28
[2025-04-28 21:22:17,248 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:17,248 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 176 transitions.
[2025-04-28 21:22:17,248 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 20 states have internal predecessors, (26), 13 states have call successors, (15), 1 states have call predecessors, (15), 10 states have return successors, (16), 10 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:22:17,249 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 176 transitions.
[2025-04-28 21:22:17,250 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:17,250 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:17,250 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]
[2025-04-28 21:22:17,257 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:17,454 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:17,454 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:17,455 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:17,455 INFO  L85        PathProgramCache]: Analyzing trace with hash -1350150074, now seen corresponding path program 1 times
[2025-04-28 21:22:17,455 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:17,455 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [116615856]
[2025-04-28 21:22:17,455 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:17,455 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:17,467 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:17,486 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:17,486 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:17,486 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,706 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:22:17,707 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:17,707 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [116615856]
[2025-04-28 21:22:17,707 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [116615856] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:17,707 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:17,707 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:22:17,708 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [582537652]
[2025-04-28 21:22:17,708 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:17,709 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:22:17,709 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:17,710 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:22:17,710 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:22:17,710 INFO  L87              Difference]: Start difference. First operand 62 states and 176 transitions. Second operand  has 9 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 5 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:22:18,153 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:18,153 INFO  L93              Difference]: Finished difference Result 68 states and 192 transitions.
[2025-04-28 21:22:18,154 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:18,154 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 5 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7) Word has length 28
[2025-04-28 21:22:18,154 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:18,155 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:22:18,155 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:22:18,156 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=29, Invalid=103, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:22:18,157 INFO  L437           NwaCegarLoop]: 63 mSDtfsCounter, 5 mSDsluCounter, 360 mSDsCounter, 0 mSdLazyCounter, 276 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 423 SdHoareTripleChecker+Invalid, 278 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 276 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:18,157 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 423 Invalid, 278 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 276 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:18,158 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:22:18,175 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 62.
[2025-04-28 21:22:18,176 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 23 states have (on average 1.391304347826087) internal successors, (32), 31 states have internal predecessors, (32), 22 states have call successors, (22), 7 states have call predecessors, (22), 16 states have return successors, (121), 23 states have call predecessors, (121), 22 states have call successors, (121)
[2025-04-28 21:22:18,177 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 175 transitions.
[2025-04-28 21:22:18,178 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 175 transitions. Word has length 28
[2025-04-28 21:22:18,180 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:18,180 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 175 transitions.
[2025-04-28 21:22:18,180 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 5 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:22:18,180 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 175 transitions.
[2025-04-28 21:22:18,182 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:22:18,183 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:18,184 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:22:18,184 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:22:18,184 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:18,184 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:18,186 INFO  L85        PathProgramCache]: Analyzing trace with hash 1432703380, now seen corresponding path program 1 times
[2025-04-28 21:22:18,186 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:18,186 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [315856894]
[2025-04-28 21:22:18,187 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:18,187 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:18,206 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:18,231 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:18,231 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:18,231 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:18,514 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:18,515 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:18,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [315856894]
[2025-04-28 21:22:18,515 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [315856894] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:18,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1092070340]
[2025-04-28 21:22:18,515 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:18,515 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:18,518 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:18,520 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:18,522 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:18,747 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:22:18,852 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:22:18,852 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:18,852 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:18,856 INFO  L256         TraceCheckSpWp]: Trace formula consists of 861 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:18,858 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:18,911 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:18,911 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
