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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:39,484 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:39,587 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_01c5b710-bcc0-4ae8-9880-3db0d0596855/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:39,594 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:39,596 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:39,619 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:39,619 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:39,619 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:39,620 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:39,620 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:39,620 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:39,620 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:39,620 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:39,621 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:39,621 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:39,621 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:39,621 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:39,621 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:39,621 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:39,621 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:39,622 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:39,622 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:39,622 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:39,622 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:39,622 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:39,623 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:39,623 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:39,942 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:39,955 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:39,957 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:39,959 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:39,959 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:39,960 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_01c5b710-bcc0-4ae8-9880-3db0d0596855/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-159.smt2
[2025-04-28 21:21:39,966 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:39,970 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:40,909 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_01c5b710-bcc0-4ae8-9880-3db0d0596855/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-159.smt2
[2025-04-28 21:21:40,913 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:40,915 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:40,916 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:40,916 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:40,916 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:40,920 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,023 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41 Unit
[2025-04-28 21:21:41,023 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:41,025 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,025 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:41,025 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:41,046 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,046 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,099 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,099 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,137 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,139 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,145 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,150 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,153 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,191 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,192 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,192 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,192 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,193 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,196 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,209 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,224 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:41,228 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:41,246 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,246 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,246 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,246 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:41,247 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:41,247 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:41,247 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_0 given in one single declaration
[2025-04-28 21:21:41,247 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_0
[2025-04-28 21:21:41,247 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_0
[2025-04-28 21:21:41,247 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:41,247 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:41,247 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:41,247 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,247 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,247 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:41,437 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:41,440 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:42,795 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:42,796 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:42,830 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:42,830 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:42,831 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42 BoogieIcfgContainer
[2025-04-28 21:21:42,831 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:42,837 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:42,837 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:42,847 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:42,847 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/3) ...
[2025-04-28 21:21:42,849 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@413f88a4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,849 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (2/3) ...
[2025-04-28 21:21:42,849 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@413f88a4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,850 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42" (3/3) ...
[2025-04-28 21:21:42,852 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:42,871 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:42,874 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 226 locations, 680 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:42,946 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:42,972 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;@c87acc3, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:42,972 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:42,981 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 226 states, 9 states have (on average 5.222222222222222) internal successors, (47), 47 states have internal predecessors, (47), 211 states have call successors, (211), 4 states have call predecessors, (211), 4 states have return successors, (211), 175 states have call predecessors, (211), 211 states have call successors, (211)
[2025-04-28 21:21:43,055 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:43,055 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,056 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,056 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,061 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,062 INFO  L85        PathProgramCache]: Analyzing trace with hash -1521844657, now seen corresponding path program 1 times
[2025-04-28 21:21:43,071 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,071 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1710731660]
[2025-04-28 21:21:43,072 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,073 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,109 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:43,130 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:43,130 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,131 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,295 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:43,295 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,295 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1710731660]
[2025-04-28 21:21:43,296 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1710731660] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,297 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,300 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:43,301 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [652688512]
[2025-04-28 21:21:43,303 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,307 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,307 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,389 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,390 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,401 INFO  L87              Difference]: Start difference. First operand  has 226 states, 9 states have (on average 5.222222222222222) internal successors, (47), 47 states have internal predecessors, (47), 211 states have call successors, (211), 4 states have call predecessors, (211), 4 states have return successors, (211), 175 states have call predecessors, (211), 211 states have call successors, (211) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:44,897 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,898 INFO  L93              Difference]: Finished difference Result 228 states and 629 transitions.
[2025-04-28 21:21:44,901 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:44,902 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:44,902 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,949 INFO  L225             Difference]: With dead ends: 228
[2025-04-28 21:21:44,949 INFO  L226             Difference]: Without dead ends: 228
[2025-04-28 21:21:44,951 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,956 INFO  L437           NwaCegarLoop]: 310 mSDtfsCounter, 1 mSDsluCounter, 424 mSDsCounter, 0 mSdLazyCounter, 669 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 734 SdHoareTripleChecker+Invalid, 669 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 669 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,958 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 734 Invalid, 669 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 669 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:44,978 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 228 states.
[2025-04-28 21:21:45,238 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 228 to 226.
[2025-04-28 21:21:45,242 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 226 states, 9 states have (on average 5.111111111111111) internal successors, (46), 46 states have internal predecessors, (46), 211 states have call successors, (211), 4 states have call predecessors, (211), 5 states have return successors, (370), 175 states have call predecessors, (370), 211 states have call successors, (370)
[2025-04-28 21:21:45,265 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 226 states to 226 states and 627 transitions.
[2025-04-28 21:21:45,269 INFO  L79                 Accepts]: Start accepts. Automaton has 226 states and 627 transitions. Word has length 12
[2025-04-28 21:21:45,270 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,270 INFO  L485      AbstractCegarLoop]: Abstraction has 226 states and 627 transitions.
[2025-04-28 21:21:45,271 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:45,271 INFO  L278                IsEmpty]: Start isEmpty. Operand 226 states and 627 transitions.
[2025-04-28 21:21:45,294 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:45,294 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,294 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,295 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,295 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,296 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,297 INFO  L85        PathProgramCache]: Analyzing trace with hash 534143349, now seen corresponding path program 1 times
[2025-04-28 21:21:45,297 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,297 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2103865505]
[2025-04-28 21:21:45,297 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,297 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,305 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:45,320 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:45,323 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,323 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,464 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,464 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2103865505]
[2025-04-28 21:21:45,465 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2103865505] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1438846018]
[2025-04-28 21:21:45,465 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,465 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,468 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,471 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:45,474 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,553 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:45,574 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:45,574 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,574 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,577 INFO  L256         TraceCheckSpWp]: Trace formula consists of 110 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,582 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,665 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,665 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,797 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,797 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1438846018] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,797 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,797 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 6, 6] total 9
[2025-04-28 21:21:45,798 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [685648718]
[2025-04-28 21:21:45,798 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,799 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:45,799 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,799 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:45,799 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:45,800 INFO  L87              Difference]: Start difference. First operand 226 states and 627 transitions. Second operand  has 9 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 2 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:47,897 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,897 INFO  L93              Difference]: Finished difference Result 232 states and 632 transitions.
[2025-04-28 21:21:47,898 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:47,898 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 2 states have call predecessors, (7), 6 states have call successors, (7) Word has length 16
[2025-04-28 21:21:47,898 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,921 INFO  L225             Difference]: With dead ends: 232
[2025-04-28 21:21:47,921 INFO  L226             Difference]: Without dead ends: 232
[2025-04-28 21:21:47,922 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 28 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=100, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:47,923 INFO  L437           NwaCegarLoop]: 313 mSDtfsCounter, 8 mSDsluCounter, 995 mSDsCounter, 0 mSdLazyCounter, 1511 mSolverCounterSat, 58 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 48 SdHoareTripleChecker+Valid, 1308 SdHoareTripleChecker+Invalid, 1569 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 58 IncrementalHoareTripleChecker+Valid, 1511 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,923 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [48 Valid, 1308 Invalid, 1569 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [58 Valid, 1511 Invalid, 0 Unknown, 0 Unchecked, 1.9s Time]
[2025-04-28 21:21:47,924 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 232 states.
[2025-04-28 21:21:48,022 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 232 to 226.
[2025-04-28 21:21:48,023 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 226 states, 9 states have (on average 5.111111111111111) internal successors, (46), 46 states have internal predecessors, (46), 211 states have call successors, (211), 4 states have call predecessors, (211), 5 states have return successors, (369), 175 states have call predecessors, (369), 211 states have call successors, (369)
[2025-04-28 21:21:48,037 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 226 states to 226 states and 626 transitions.
[2025-04-28 21:21:48,037 INFO  L79                 Accepts]: Start accepts. Automaton has 226 states and 626 transitions. Word has length 16
[2025-04-28 21:21:48,037 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,037 INFO  L485      AbstractCegarLoop]: Abstraction has 226 states and 626 transitions.
[2025-04-28 21:21:48,037 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 2 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:48,038 INFO  L278                IsEmpty]: Start isEmpty. Operand 226 states and 626 transitions.
[2025-04-28 21:21:48,056 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:48,056 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,056 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,062 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:48,257 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,257 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,257 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,258 INFO  L85        PathProgramCache]: Analyzing trace with hash -1218577390, now seen corresponding path program 1 times
[2025-04-28 21:21:48,258 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,258 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1120861072]
[2025-04-28 21:21:48,258 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,258 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,264 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:48,269 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:48,269 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,269 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,363 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:48,363 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,364 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1120861072]
[2025-04-28 21:21:48,364 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1120861072] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,364 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2141259108]
[2025-04-28 21:21:48,364 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,364 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,368 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,370 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:48,397 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,463 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:48,481 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:48,481 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,481 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,482 INFO  L256         TraceCheckSpWp]: Trace formula consists of 109 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,483 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,519 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:48,520 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:48,520 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2141259108] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,520 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:48,520 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:48,520 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1116619764]
[2025-04-28 21:21:48,520 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,521 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:48,521 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,521 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:48,521 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,521 INFO  L87              Difference]: Start difference. First operand 226 states and 626 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:49,611 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,611 INFO  L93              Difference]: Finished difference Result 228 states and 627 transitions.
[2025-04-28 21:21:49,612 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:49,613 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:21:49,613 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,631 INFO  L225             Difference]: With dead ends: 228
[2025-04-28 21:21:49,631 INFO  L226             Difference]: Without dead ends: 228
[2025-04-28 21:21:49,631 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 15 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:49,633 INFO  L437           NwaCegarLoop]: 312 mSDtfsCounter, 1 mSDsluCounter, 430 mSDsCounter, 0 mSdLazyCounter, 660 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 742 SdHoareTripleChecker+Invalid, 660 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 660 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,633 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 742 Invalid, 660 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 660 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:49,634 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 228 states.
[2025-04-28 21:21:49,717 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 228 to 226.
[2025-04-28 21:21:49,718 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 226 states, 9 states have (on average 5.111111111111111) internal successors, (46), 46 states have internal predecessors, (46), 211 states have call successors, (211), 4 states have call predecessors, (211), 5 states have return successors, (368), 175 states have call predecessors, (368), 211 states have call successors, (368)
[2025-04-28 21:21:49,737 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 226 states to 226 states and 625 transitions.
[2025-04-28 21:21:49,737 INFO  L79                 Accepts]: Start accepts. Automaton has 226 states and 625 transitions. Word has length 16
[2025-04-28 21:21:49,737 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,737 INFO  L485      AbstractCegarLoop]: Abstraction has 226 states and 625 transitions.
[2025-04-28 21:21:49,737 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:49,738 INFO  L278                IsEmpty]: Start isEmpty. Operand 226 states and 625 transitions.
[2025-04-28 21:21:49,751 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:49,751 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,752 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,757 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:49,955 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,955 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,956 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,956 INFO  L85        PathProgramCache]: Analyzing trace with hash 106126375, now seen corresponding path program 1 times
[2025-04-28 21:21:49,956 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,956 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [896064037]
[2025-04-28 21:21:49,956 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,956 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,962 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:50,013 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:50,014 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,014 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:50,280 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [896064037]
[2025-04-28 21:21:50,280 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [896064037] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [636686763]
[2025-04-28 21:21:50,280 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,280 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,283 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,285 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:50,288 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,344 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:50,360 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:50,360 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,361 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,362 INFO  L256         TraceCheckSpWp]: Trace formula consists of 109 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,363 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,448 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 3 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:50,449 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:50,449 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [636686763] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,449 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:50,449 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:50,449 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1548135761]
[2025-04-28 21:21:50,449 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,450 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,450 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,450 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,450 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,451 INFO  L87              Difference]: Start difference. First operand 226 states and 625 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:51,616 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,616 INFO  L93              Difference]: Finished difference Result 228 states and 626 transitions.
[2025-04-28 21:21:51,618 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:51,618 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:51,619 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,636 INFO  L225             Difference]: With dead ends: 228
[2025-04-28 21:21:51,637 INFO  L226             Difference]: Without dead ends: 228
[2025-04-28 21:21:51,637 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 15 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:51,639 INFO  L437           NwaCegarLoop]: 313 mSDtfsCounter, 1 mSDsluCounter, 430 mSDsCounter, 0 mSdLazyCounter, 659 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 743 SdHoareTripleChecker+Invalid, 659 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 659 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,639 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 743 Invalid, 659 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 659 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:51,640 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 228 states.
[2025-04-28 21:21:51,730 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 228 to 226.
[2025-04-28 21:21:51,730 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 226 states, 9 states have (on average 5.111111111111111) internal successors, (46), 46 states have internal predecessors, (46), 211 states have call successors, (211), 4 states have call predecessors, (211), 5 states have return successors, (367), 175 states have call predecessors, (367), 211 states have call successors, (367)
[2025-04-28 21:21:51,739 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 226 states to 226 states and 624 transitions.
[2025-04-28 21:21:51,740 INFO  L79                 Accepts]: Start accepts. Automaton has 226 states and 624 transitions. Word has length 16
[2025-04-28 21:21:51,740 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,740 INFO  L485      AbstractCegarLoop]: Abstraction has 226 states and 624 transitions.
[2025-04-28 21:21:51,740 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:51,740 INFO  L278                IsEmpty]: Start isEmpty. Operand 226 states and 624 transitions.
[2025-04-28 21:21:51,752 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:51,752 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,752 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,758 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,953 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,954 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,955 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,955 INFO  L85        PathProgramCache]: Analyzing trace with hash 1973277573, now seen corresponding path program 1 times
[2025-04-28 21:21:51,955 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1146159284]
[2025-04-28 21:21:51,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,955 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,962 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:51,971 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:51,973 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,973 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,168 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:52,168 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,169 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1146159284]
[2025-04-28 21:21:52,169 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1146159284] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,169 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1874392436]
[2025-04-28 21:21:52,169 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,169 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,172 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,174 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,180 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,236 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:52,252 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:52,252 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,253 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,254 INFO  L256         TraceCheckSpWp]: Trace formula consists of 109 conjuncts, 26 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,255 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,334 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 3 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:52,334 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:52,334 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1874392436] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,334 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:52,335 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:21:52,335 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [572703248]
[2025-04-28 21:21:52,335 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,335 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:52,335 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,336 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:52,336 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,336 INFO  L87              Difference]: Start difference. First operand 226 states and 624 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:53,354 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,354 INFO  L93              Difference]: Finished difference Result 228 states and 625 transitions.
[2025-04-28 21:21:53,357 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:53,357 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:53,358 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,372 INFO  L225             Difference]: With dead ends: 228
[2025-04-28 21:21:53,373 INFO  L226             Difference]: Without dead ends: 228
[2025-04-28 21:21:53,373 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 19 GetRequests, 15 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,374 INFO  L437           NwaCegarLoop]: 314 mSDtfsCounter, 1 mSDsluCounter, 432 mSDsCounter, 0 mSdLazyCounter, 656 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 746 SdHoareTripleChecker+Invalid, 656 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 656 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,374 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 746 Invalid, 656 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 656 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:53,375 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 228 states.
[2025-04-28 21:21:53,444 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 228 to 226.
[2025-04-28 21:21:53,445 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 226 states, 9 states have (on average 5.111111111111111) internal successors, (46), 46 states have internal predecessors, (46), 211 states have call successors, (211), 4 states have call predecessors, (211), 5 states have return successors, (366), 175 states have call predecessors, (366), 211 states have call successors, (366)
[2025-04-28 21:21:53,455 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 226 states to 226 states and 623 transitions.
[2025-04-28 21:21:53,455 INFO  L79                 Accepts]: Start accepts. Automaton has 226 states and 623 transitions. Word has length 16
[2025-04-28 21:21:53,456 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,456 INFO  L485      AbstractCegarLoop]: Abstraction has 226 states and 623 transitions.
[2025-04-28 21:21:53,456 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:53,456 INFO  L278                IsEmpty]: Start isEmpty. Operand 226 states and 623 transitions.
[2025-04-28 21:21:53,481 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:53,481 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,482 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,487 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:53,684 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:53,685 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,685 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,685 INFO  L85        PathProgramCache]: Analyzing trace with hash 1246465418, now seen corresponding path program 1 times
[2025-04-28 21:21:53,685 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,685 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [347275688]
[2025-04-28 21:21:53,686 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,686 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,691 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:53,695 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:53,696 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,696 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,938 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:53,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [347275688]
[2025-04-28 21:21:53,938 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [347275688] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [694978307]
[2025-04-28 21:21:53,938 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,939 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,941 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,943 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,947 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,013 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,041 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,041 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,042 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,044 INFO  L256         TraceCheckSpWp]: Trace formula consists of 217 conjuncts, 59 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,046 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,255 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 9 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:54,255 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,777 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:54,777 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [694978307] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,777 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,777 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 12
[2025-04-28 21:21:54,777 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [584890461]
[2025-04-28 21:21:54,777 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,778 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:54,778 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,778 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:54,778 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=97, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:54,779 INFO  L87              Difference]: Start difference. First operand 226 states and 623 transitions. Second operand  has 12 states, 4 states have (on average 3.5) internal successors, (14), 7 states have internal predecessors, (14), 10 states have call successors, (12), 2 states have call predecessors, (12), 4 states have return successors, (12), 6 states have call predecessors, (12), 10 states have call successors, (12)
[2025-04-28 21:21:58,981 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,982 INFO  L93              Difference]: Finished difference Result 355 states and 994 transitions.
[2025-04-28 21:21:58,982 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:58,983 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 4 states have (on average 3.5) internal successors, (14), 7 states have internal predecessors, (14), 10 states have call successors, (12), 2 states have call predecessors, (12), 4 states have return successors, (12), 6 states have call predecessors, (12), 10 states have call successors, (12) Word has length 24
[2025-04-28 21:21:58,983 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,012 INFO  L225             Difference]: With dead ends: 355
[2025-04-28 21:21:59,012 INFO  L226             Difference]: Without dead ends: 355
[2025-04-28 21:21:59,012 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 45 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=58, Invalid=152, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:59,014 INFO  L437           NwaCegarLoop]: 436 mSDtfsCounter, 25 mSDsluCounter, 1863 mSDsCounter, 0 mSdLazyCounter, 3246 mSolverCounterSat, 29 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 3.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 259 SdHoareTripleChecker+Valid, 2299 SdHoareTripleChecker+Invalid, 3275 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 29 IncrementalHoareTripleChecker+Valid, 3246 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 4.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,014 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [259 Valid, 2299 Invalid, 3275 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [29 Valid, 3246 Invalid, 0 Unknown, 0 Unchecked, 4.0s Time]
[2025-04-28 21:21:59,015 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 355 states.
[2025-04-28 21:21:59,206 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 355 to 345.
[2025-04-28 21:21:59,208 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 345 states, 11 states have (on average 5.818181818181818) internal successors, (64), 63 states have internal predecessors, (64), 327 states have call successors, (327), 5 states have call predecessors, (327), 6 states have return successors, (589), 276 states have call predecessors, (589), 327 states have call successors, (589)
[2025-04-28 21:21:59,223 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 345 states to 345 states and 980 transitions.
[2025-04-28 21:21:59,223 INFO  L79                 Accepts]: Start accepts. Automaton has 345 states and 980 transitions. Word has length 24
[2025-04-28 21:21:59,223 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,224 INFO  L485      AbstractCegarLoop]: Abstraction has 345 states and 980 transitions.
[2025-04-28 21:21:59,224 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 4 states have (on average 3.5) internal successors, (14), 7 states have internal predecessors, (14), 10 states have call successors, (12), 2 states have call predecessors, (12), 4 states have return successors, (12), 6 states have call predecessors, (12), 10 states have call successors, (12)
[2025-04-28 21:21:59,224 INFO  L278                IsEmpty]: Start isEmpty. Operand 345 states and 980 transitions.
[2025-04-28 21:21:59,242 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:59,242 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,242 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,247 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:59,446 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,446 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,448 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,448 INFO  L85        PathProgramCache]: Analyzing trace with hash -1442139798, now seen corresponding path program 1 times
[2025-04-28 21:21:59,448 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,449 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1886395234]
[2025-04-28 21:21:59,449 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,449 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,454 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:59,466 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:59,466 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,466 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,839 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:59,840 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,840 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1886395234]
[2025-04-28 21:21:59,840 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1886395234] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:59,840 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [925957159]
[2025-04-28 21:21:59,840 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,840 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,843 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:59,844 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:59,848 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:59,911 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:59,939 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:59,939 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,939 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,941 INFO  L256         TraceCheckSpWp]: Trace formula consists of 216 conjuncts, 59 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:59,943 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,071 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 9 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,071 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:00,562 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:00,562 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [925957159] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,562 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,562 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 11
[2025-04-28 21:22:00,562 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [762134542]
[2025-04-28 21:22:00,562 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,563 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:22:00,563 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,563 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:22:00,564 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=80, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:00,564 INFO  L87              Difference]: Start difference. First operand 345 states and 980 transitions. Second operand  has 11 states, 4 states have (on average 3.5) internal successors, (14), 7 states have internal predecessors, (14), 9 states have call successors, (11), 2 states have call predecessors, (11), 4 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:22:02,416 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,416 INFO  L93              Difference]: Finished difference Result 356 states and 1000 transitions.
[2025-04-28 21:22:02,417 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:02,417 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 4 states have (on average 3.5) internal successors, (14), 7 states have internal predecessors, (14), 9 states have call successors, (11), 2 states have call predecessors, (11), 4 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11) Word has length 24
[2025-04-28 21:22:02,417 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,439 INFO  L225             Difference]: With dead ends: 356
[2025-04-28 21:22:02,439 INFO  L226             Difference]: Without dead ends: 356
[2025-04-28 21:22:02,439 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 46 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=52, Invalid=130, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:22:02,440 INFO  L437           NwaCegarLoop]: 316 mSDtfsCounter, 9 mSDsluCounter, 1172 mSDsCounter, 0 mSdLazyCounter, 1334 mSolverCounterSat, 37 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 1488 SdHoareTripleChecker+Invalid, 1371 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 37 IncrementalHoareTripleChecker+Valid, 1334 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,440 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 1488 Invalid, 1371 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [37 Valid, 1334 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:22:02,441 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 356 states.
[2025-04-28 21:22:02,609 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 356 to 347.
[2025-04-28 21:22:02,610 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 347 states, 11 states have (on average 5.818181818181818) internal successors, (64), 63 states have internal predecessors, (64), 329 states have call successors, (329), 5 states have call predecessors, (329), 6 states have return successors, (592), 278 states have call predecessors, (592), 329 states have call successors, (592)
[2025-04-28 21:22:02,625 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 347 states to 347 states and 985 transitions.
[2025-04-28 21:22:02,625 INFO  L79                 Accepts]: Start accepts. Automaton has 347 states and 985 transitions. Word has length 24
[2025-04-28 21:22:02,626 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,626 INFO  L485      AbstractCegarLoop]: Abstraction has 347 states and 985 transitions.
[2025-04-28 21:22:02,626 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 4 states have (on average 3.5) internal successors, (14), 7 states have internal predecessors, (14), 9 states have call successors, (11), 2 states have call predecessors, (11), 4 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:22:02,626 INFO  L278                IsEmpty]: Start isEmpty. Operand 347 states and 985 transitions.
[2025-04-28 21:22:02,645 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:02,645 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,645 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:02,650 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:02,849 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,850 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,850 INFO  L85        PathProgramCache]: Analyzing trace with hash 2031587000, now seen corresponding path program 1 times
[2025-04-28 21:22:02,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,850 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [228808906]
[2025-04-28 21:22:02,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,857 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:02,863 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:02,863 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,863 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,930 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:02,930 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,930 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [228808906]
[2025-04-28 21:22:02,930 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [228808906] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,931 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [299919254]
[2025-04-28 21:22:02,931 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,931 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,933 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,935 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:02,939 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:03,005 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:03,035 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:03,035 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,035 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,039 INFO  L256         TraceCheckSpWp]: Trace formula consists of 214 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:03,041 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:03,067 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 13 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:03,067 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:03,067 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [299919254] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,067 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:03,067 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:22:03,068 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [409208456]
[2025-04-28 21:22:03,068 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,068 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:03,068 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,068 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:03,068 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:03,069 INFO  L87              Difference]: Start difference. First operand 347 states and 985 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 2 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:04,003 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,003 INFO  L93              Difference]: Finished difference Result 349 states and 986 transitions.
[2025-04-28 21:22:04,003 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:04,004 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 2 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:22:04,004 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,024 INFO  L225             Difference]: With dead ends: 349
[2025-04-28 21:22:04,024 INFO  L226             Difference]: Without dead ends: 349
[2025-04-28 21:22:04,025 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 27 GetRequests, 25 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:04,025 INFO  L437           NwaCegarLoop]: 317 mSDtfsCounter, 1 mSDsluCounter, 438 mSDsCounter, 0 mSdLazyCounter, 651 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 755 SdHoareTripleChecker+Invalid, 651 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 651 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,025 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 755 Invalid, 651 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 651 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:04,026 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 349 states.
[2025-04-28 21:22:04,194 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 349 to 347.
[2025-04-28 21:22:04,195 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 347 states, 11 states have (on average 5.818181818181818) internal successors, (64), 63 states have internal predecessors, (64), 329 states have call successors, (329), 5 states have call predecessors, (329), 6 states have return successors, (591), 278 states have call predecessors, (591), 329 states have call successors, (591)
[2025-04-28 21:22:04,209 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 347 states to 347 states and 984 transitions.
[2025-04-28 21:22:04,209 INFO  L79                 Accepts]: Start accepts. Automaton has 347 states and 984 transitions. Word has length 24
[2025-04-28 21:22:04,209 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,210 INFO  L485      AbstractCegarLoop]: Abstraction has 347 states and 984 transitions.
[2025-04-28 21:22:04,210 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 2 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:22:04,210 INFO  L278                IsEmpty]: Start isEmpty. Operand 347 states and 984 transitions.
[2025-04-28 21:22:04,225 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:22:04,225 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,225 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,230 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:04,429 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:22:04,429 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,430 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,430 INFO  L85        PathProgramCache]: Analyzing trace with hash 1955264055, now seen corresponding path program 1 times
[2025-04-28 21:22:04,430 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,430 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [991568093]
[2025-04-28 21:22:04,430 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,430 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,435 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:04,438 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:04,438 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,438 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,502 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:04,502 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,502 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [991568093]
[2025-04-28 21:22:04,503 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [991568093] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,503 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1761725781]
[2025-04-28 21:22:04,503 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,503 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,505 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,507 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:04,510 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,577 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:22:04,609 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:22:04,609 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,609 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,614 INFO  L256         TraceCheckSpWp]: Trace formula consists of 217 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,615 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:04,667 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:04,669 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:04,786 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:04,787 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1761725781] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:04,787 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:04,787 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 6, 6] total 9
[2025-04-28 21:22:04,787 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2053002693]
[2025-04-28 21:22:04,787 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,787 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:22:04,787 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,788 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:22:04,788 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:22:04,788 INFO  L87              Difference]: Start difference. First operand 347 states and 984 transitions. Second operand  has 9 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 6 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 2 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:22:06,177 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,178 INFO  L93              Difference]: Finished difference Result 351 states and 987 transitions.
[2025-04-28 21:22:06,178 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:06,179 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 6 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 2 states have call predecessors, (11), 6 states have call successors, (11) Word has length 24
[2025-04-28 21:22:06,179 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,196 INFO  L225             Difference]: With dead ends: 351
[2025-04-28 21:22:06,196 INFO  L226             Difference]: Without dead ends: 351
[2025-04-28 21:22:06,196 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 53 GetRequests, 44 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=27, Invalid=83, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:22:06,197 INFO  L437           NwaCegarLoop]: 318 mSDtfsCounter, 4 mSDsluCounter, 1325 mSDsCounter, 0 mSdLazyCounter, 1626 mSolverCounterSat, 37 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 1643 SdHoareTripleChecker+Invalid, 1663 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 37 IncrementalHoareTripleChecker+Valid, 1626 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,197 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 1643 Invalid, 1663 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [37 Valid, 1626 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:22:06,198 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 351 states.
[2025-04-28 21:22:06,363 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 351 to 347.
[2025-04-28 21:22:06,366 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 347 states, 11 states have (on average 5.818181818181818) internal successors, (64), 63 states have internal predecessors, (64), 329 states have call successors, (329), 5 states have call predecessors, (329), 6 states have return successors, (590), 278 states have call predecessors, (590), 329 states have call successors, (590)
[2025-04-28 21:22:06,386 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 347 states to 347 states and 983 transitions.
[2025-04-28 21:22:06,386 INFO  L79                 Accepts]: Start accepts. Automaton has 347 states and 983 transitions. Word has length 24
[2025-04-28 21:22:06,387 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,387 INFO  L485      AbstractCegarLoop]: Abstraction has 347 states and 983 transitions.
[2025-04-28 21:22:06,388 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 6 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 2 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:22:06,388 INFO  L278                IsEmpty]: Start isEmpty. Operand 347 states and 983 transitions.
[2025-04-28 21:22:06,413 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:06,413 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,413 INFO  L218           NwaCegarLoop]: trace histogram [6, 6, 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:06,418 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:06,617 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:06,618 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,619 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,619 INFO  L85        PathProgramCache]: Analyzing trace with hash 907977579, now seen corresponding path program 1 times
[2025-04-28 21:22:06,619 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,619 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [66395921]
[2025-04-28 21:22:06,619 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,619 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,627 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:06,632 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:06,632 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,632 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,700 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 2 proven. 8 refuted. 0 times theorem prover too weak. 35 trivial. 0 not checked.
[2025-04-28 21:22:06,701 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,701 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [66395921]
[2025-04-28 21:22:06,701 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [66395921] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,701 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [813110044]
[2025-04-28 21:22:06,701 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,701 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,704 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,706 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:06,709 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,786 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:06,834 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:06,834 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,834 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,839 INFO  L256         TraceCheckSpWp]: Trace formula consists of 322 conjuncts, 30 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,841 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:06,958 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 31 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:06,958 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:06,958 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [813110044] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:06,958 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:06,958 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 6
[2025-04-28 21:22:06,958 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [534356068]
[2025-04-28 21:22:06,958 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,959 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:06,959 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,959 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:06,959 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:06,959 INFO  L87              Difference]: Start difference. First operand 347 states and 983 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:07,983 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,983 INFO  L93              Difference]: Finished difference Result 349 states and 984 transitions.
[2025-04-28 21:22:07,984 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:07,984 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:22:07,984 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,997 INFO  L225             Difference]: With dead ends: 349
[2025-04-28 21:22:07,997 INFO  L226             Difference]: Without dead ends: 349
[2025-04-28 21:22:07,998 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 35 GetRequests, 31 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:07,998 INFO  L437           NwaCegarLoop]: 319 mSDtfsCounter, 1 mSDsluCounter, 442 mSDsCounter, 0 mSdLazyCounter, 643 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 761 SdHoareTripleChecker+Invalid, 643 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 643 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,998 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 761 Invalid, 643 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 643 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:22:07,999 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 349 states.
[2025-04-28 21:22:08,132 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 349 to 347.
[2025-04-28 21:22:08,133 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 347 states, 11 states have (on average 5.818181818181818) internal successors, (64), 63 states have internal predecessors, (64), 329 states have call successors, (329), 5 states have call predecessors, (329), 6 states have return successors, (589), 278 states have call predecessors, (589), 329 states have call successors, (589)
[2025-04-28 21:22:08,148 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 347 states to 347 states and 982 transitions.
[2025-04-28 21:22:08,149 INFO  L79                 Accepts]: Start accepts. Automaton has 347 states and 982 transitions. Word has length 32
[2025-04-28 21:22:08,149 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,149 INFO  L485      AbstractCegarLoop]: Abstraction has 347 states and 982 transitions.
[2025-04-28 21:22:08,149 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:08,149 INFO  L278                IsEmpty]: Start isEmpty. Operand 347 states and 982 transitions.
[2025-04-28 21:22:08,166 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:08,166 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,167 INFO  L218           NwaCegarLoop]: trace histogram [6, 6, 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:08,170 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:08,367 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:22:08,367 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,367 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,368 INFO  L85        PathProgramCache]: Analyzing trace with hash 98307451, now seen corresponding path program 1 times
[2025-04-28 21:22:08,368 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,368 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [384179104]
[2025-04-28 21:22:08,368 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,368 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,374 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:08,378 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:08,378 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,378 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,437 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 2 proven. 8 refuted. 0 times theorem prover too weak. 35 trivial. 0 not checked.
[2025-04-28 21:22:08,437 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,437 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [384179104]
[2025-04-28 21:22:08,438 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [384179104] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:08,438 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1104373534]
[2025-04-28 21:22:08,438 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,438 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,440 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:08,442 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:08,445 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:08,524 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:08,571 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:08,571 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,573 INFO  L256         TraceCheckSpWp]: Trace formula consists of 323 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:08,574 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,604 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 26 proven. 0 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:22:08,605 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:22:08,605 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1104373534] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:08,605 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:22:08,605 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:22:08,605 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [564666637]
[2025-04-28 21:22:08,605 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,606 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:08,606 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,606 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:08,606 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:08,606 INFO  L87              Difference]: Start difference. First operand 347 states and 982 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:09,533 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,533 INFO  L93              Difference]: Finished difference Result 349 states and 983 transitions.
[2025-04-28 21:22:09,533 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:09,534 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:22:09,534 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,550 INFO  L225             Difference]: With dead ends: 349
[2025-04-28 21:22:09,550 INFO  L226             Difference]: Without dead ends: 349
[2025-04-28 21:22:09,551 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 35 GetRequests, 33 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:09,552 INFO  L437           NwaCegarLoop]: 320 mSDtfsCounter, 1 mSDsluCounter, 446 mSDsCounter, 0 mSdLazyCounter, 638 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 766 SdHoareTripleChecker+Invalid, 638 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 638 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,552 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 766 Invalid, 638 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 638 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:22:09,554 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 349 states.
[2025-04-28 21:22:09,661 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 349 to 347.
[2025-04-28 21:22:09,662 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 347 states, 11 states have (on average 5.818181818181818) internal successors, (64), 63 states have internal predecessors, (64), 329 states have call successors, (329), 5 states have call predecessors, (329), 6 states have return successors, (588), 278 states have call predecessors, (588), 329 states have call successors, (588)
[2025-04-28 21:22:09,676 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 347 states to 347 states and 981 transitions.
[2025-04-28 21:22:09,676 INFO  L79                 Accepts]: Start accepts. Automaton has 347 states and 981 transitions. Word has length 32
[2025-04-28 21:22:09,676 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,676 INFO  L485      AbstractCegarLoop]: Abstraction has 347 states and 981 transitions.
[2025-04-28 21:22:09,676 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:09,676 INFO  L278                IsEmpty]: Start isEmpty. Operand 347 states and 981 transitions.
[2025-04-28 21:22:09,701 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:09,702 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,702 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 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,707 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:09,906 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,906 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,907 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,907 INFO  L85        PathProgramCache]: Analyzing trace with hash -336234933, now seen corresponding path program 1 times
[2025-04-28 21:22:09,907 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,907 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [604853487]
[2025-04-28 21:22:09,907 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:09,907 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,914 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:09,930 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:09,931 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,931 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
