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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:38,450 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:38,561 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_21a41bbd-74ad-4304-9028-6f1c89373621/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:38,570 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:38,570 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:38,606 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:38,608 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:38,608 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:38,610 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:38,610 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:38,611 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:38,612 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:38,612 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:38,612 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:38,612 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:38,613 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:38,613 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:38,613 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:38,613 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:38,613 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:38,614 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:38,614 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:38,614 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:38,614 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:38,614 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:38,615 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:38,615 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:38,974 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:38,985 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:38,990 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:38,993 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:38,994 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:38,995 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_21a41bbd-74ad-4304-9028-6f1c89373621/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-172.smt2
[2025-04-28 21:21:38,997 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:39,002 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:39,288 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_21a41bbd-74ad-4304-9028-6f1c89373621/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-172.smt2
[2025-04-28 21:21:39,292 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:39,294 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:39,294 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:39,295 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:39,295 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:39,301 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,334 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39 Unit
[2025-04-28 21:21:39,335 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:39,336 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:39,336 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:39,336 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:39,357 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,357 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,379 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,380 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,383 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,384 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,387 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,388 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,389 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,402 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:39,403 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:39,403 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:39,403 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:39,404 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,407 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:39,426 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,443 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:39,451 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:39,465 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:39,465 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:39,465 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:39,466 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure END_QUERY given in one single declaration
[2025-04-28 21:21:39,466 INFO  L130     BoogieDeclarations]: Found specification of procedure END_QUERY
[2025-04-28 21:21:39,466 INFO  L138     BoogieDeclarations]: Found implementation of procedure END_QUERY
[2025-04-28 21:21:39,466 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_REC_f__1 given in one single declaration
[2025-04-28 21:21:39,466 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_REC_f__1
[2025-04-28 21:21:39,466 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_REC_f__1
[2025-04-28 21:21:39,466 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_REC_f__1_PRE given in one single declaration
[2025-04-28 21:21:39,466 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_REC_f__1_PRE
[2025-04-28 21:21:39,466 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_REC_f__1_PRE
[2025-04-28 21:21:39,468 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_REC_f^f_PRE given in one single declaration
[2025-04-28 21:21:39,468 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_REC_f^f_PRE
[2025-04-28 21:21:39,468 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_REC_f^f_PRE
[2025-04-28 21:21:39,468 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_REC_f__2 given in one single declaration
[2025-04-28 21:21:39,468 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_REC_f__2
[2025-04-28 21:21:39,469 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_REC_f__2
[2025-04-28 21:21:39,469 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_REC_f__2_PRE given in one single declaration
[2025-04-28 21:21:39,469 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_REC_f__2_PRE
[2025-04-28 21:21:39,469 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_REC_f__2_PRE
[2025-04-28 21:21:39,469 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_REC_f^f given in one single declaration
[2025-04-28 21:21:39,469 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_REC_f^f
[2025-04-28 21:21:39,469 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_REC_f^f
[2025-04-28 21:21:39,469 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:39,469 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:39,471 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:39,535 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:39,537 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:39,836 INFO  L?                        ?]: Removed 8 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:39,838 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:39,857 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:39,860 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:39,860 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:39 BoogieIcfgContainer
[2025-04-28 21:21:39,860 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:39,863 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:39,864 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:39,869 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:39,869 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:39" (1/3) ...
[2025-04-28 21:21:39,870 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@381e2b7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:39, skipping insertion in model container
[2025-04-28 21:21:39,870 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (2/3) ...
[2025-04-28 21:21:39,871 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@381e2b7 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:39, skipping insertion in model container
[2025-04-28 21:21:39,871 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:39" (3/3) ...
[2025-04-28 21:21:39,873 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:39,890 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:39,893 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 9 procedures, 56 locations, 124 edges, 9 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:39,950 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:39,977 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;@7531ad6, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:39,977 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:39,982 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 56 states, 17 states have (on average 2.176470588235294) internal successors, (37), 36 states have internal predecessors, (37), 29 states have call successors, (29), 8 states have call predecessors, (29), 8 states have return successors, (29), 15 states have call predecessors, (29), 29 states have call successors, (29)
[2025-04-28 21:21:39,997 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 9
[2025-04-28 21:21:39,999 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,000 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,000 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,006 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,007 INFO  L85        PathProgramCache]: Analyzing trace with hash 1016927239, now seen corresponding path program 1 times
[2025-04-28 21:21:40,017 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,018 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [139809278]
[2025-04-28 21:21:40,019 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,019 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,052 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 8 statements into 1 equivalence classes.
[2025-04-28 21:21:40,054 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 8 of 8 statements.
[2025-04-28 21:21:40,055 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,056 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,096 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:40,097 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,098 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [139809278]
[2025-04-28 21:21:40,099 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [139809278] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,099 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,102 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:40,105 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1088267601]
[2025-04-28 21:21:40,106 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,112 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:40,112 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,149 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:40,150 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:40,152 INFO  L87              Difference]: Start difference. First operand  has 56 states, 17 states have (on average 2.176470588235294) internal successors, (37), 36 states have internal predecessors, (37), 29 states have call successors, (29), 8 states have call predecessors, (29), 8 states have return successors, (29), 15 states have call predecessors, (29), 29 states have call successors, (29) Second operand  has 2 states, 2 states have (on average 2.0) internal successors, (4), 1 states have internal predecessors, (4), 1 states have call successors, (2), 1 states have call predecessors, (2), 1 states have return successors, (2), 1 states have call predecessors, (2), 1 states have call successors, (2)
[2025-04-28 21:21:40,179 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,180 INFO  L93              Difference]: Finished difference Result 52 states and 84 transitions.
[2025-04-28 21:21:40,181 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:40,183 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 2.0) internal successors, (4), 1 states have internal predecessors, (4), 1 states have call successors, (2), 1 states have call predecessors, (2), 1 states have return successors, (2), 1 states have call predecessors, (2), 1 states have call successors, (2) Word has length 8
[2025-04-28 21:21:40,184 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,193 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:40,194 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:40,197 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:40,204 INFO  L437           NwaCegarLoop]: 84 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 84 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,205 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 84 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:40,225 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:40,248 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 52.
[2025-04-28 21:21:40,249 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 16 states have (on average 1.875) internal successors, (30), 30 states have internal predecessors, (30), 27 states have call successors, (27), 8 states have call predecessors, (27), 8 states have return successors, (27), 15 states have call predecessors, (27), 27 states have call successors, (27)
[2025-04-28 21:21:40,255 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 84 transitions.
[2025-04-28 21:21:40,257 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 84 transitions. Word has length 8
[2025-04-28 21:21:40,257 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,257 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 84 transitions.
[2025-04-28 21:21:40,257 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 2.0) internal successors, (4), 1 states have internal predecessors, (4), 1 states have call successors, (2), 1 states have call predecessors, (2), 1 states have return successors, (2), 1 states have call predecessors, (2), 1 states have call successors, (2)
[2025-04-28 21:21:40,258 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 84 transitions.
[2025-04-28 21:21:40,263 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:40,263 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,264 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,264 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:40,264 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,265 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,265 INFO  L85        PathProgramCache]: Analyzing trace with hash -1634958726, now seen corresponding path program 1 times
[2025-04-28 21:21:40,265 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,265 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1500342456]
[2025-04-28 21:21:40,265 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,265 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,274 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:40,292 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:40,292 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,292 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,581 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:40,581 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,581 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1500342456]
[2025-04-28 21:21:40,581 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1500342456] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,581 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,582 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:40,582 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1704970065]
[2025-04-28 21:21:40,582 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,583 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:40,583 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,584 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:40,584 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:40,584 INFO  L87              Difference]: Start difference. First operand 52 states and 84 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:40,651 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,651 INFO  L93              Difference]: Finished difference Result 56 states and 90 transitions.
[2025-04-28 21:21:40,652 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:40,652 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), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:40,652 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,654 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:40,654 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:40,654 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:40,655 INFO  L437           NwaCegarLoop]: 83 mSDtfsCounter, 1 mSDsluCounter, 155 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 238 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,656 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 238 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:40,657 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:40,667 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 54.
[2025-04-28 21:21:40,667 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 54 states, 17 states have (on average 1.8235294117647058) internal successors, (31), 31 states have internal predecessors, (31), 27 states have call successors, (27), 8 states have call predecessors, (27), 9 states have return successors, (30), 16 states have call predecessors, (30), 27 states have call successors, (30)
[2025-04-28 21:21:40,669 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 88 transitions.
[2025-04-28 21:21:40,669 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 88 transitions. Word has length 16
[2025-04-28 21:21:40,670 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,670 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 88 transitions.
[2025-04-28 21:21:40,670 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), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:40,671 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 88 transitions.
[2025-04-28 21:21:40,672 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:40,672 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,672 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,673 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:40,673 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,673 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,673 INFO  L85        PathProgramCache]: Analyzing trace with hash 204464120, now seen corresponding path program 1 times
[2025-04-28 21:21:40,674 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,674 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1181064821]
[2025-04-28 21:21:40,674 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,674 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,680 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:40,697 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:40,700 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,700 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,840 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:40,840 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,840 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1181064821]
[2025-04-28 21:21:40,841 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1181064821] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,841 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,841 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:40,841 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1364715069]
[2025-04-28 21:21:40,841 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,841 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:40,841 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,842 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:40,842 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:40,842 INFO  L87              Difference]: Start difference. First operand 54 states and 88 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:40,902 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,902 INFO  L93              Difference]: Finished difference Result 58 states and 92 transitions.
[2025-04-28 21:21:40,903 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:40,903 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), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:40,903 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,905 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:21:40,905 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:21:40,905 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:40,906 INFO  L437           NwaCegarLoop]: 83 mSDtfsCounter, 1 mSDsluCounter, 152 mSDsCounter, 0 mSdLazyCounter, 10 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 235 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 10 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,907 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 235 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 10 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:40,908 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:21:40,919 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 56.
[2025-04-28 21:21:40,921 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 18 states have (on average 1.7777777777777777) internal successors, (32), 32 states have internal predecessors, (32), 27 states have call successors, (27), 8 states have call predecessors, (27), 10 states have return successors, (31), 17 states have call predecessors, (31), 27 states have call successors, (31)
[2025-04-28 21:21:40,923 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 90 transitions.
[2025-04-28 21:21:40,923 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 90 transitions. Word has length 16
[2025-04-28 21:21:40,924 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,924 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 90 transitions.
[2025-04-28 21:21:40,924 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), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:40,924 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 90 transitions.
[2025-04-28 21:21:40,934 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:40,934 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,934 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,934 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:40,935 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,935 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,936 INFO  L85        PathProgramCache]: Analyzing trace with hash 1857460103, now seen corresponding path program 1 times
[2025-04-28 21:21:40,936 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,936 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [224825405]
[2025-04-28 21:21:40,936 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,936 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,946 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:40,974 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:40,978 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,978 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,177 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:41,177 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,177 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [224825405]
[2025-04-28 21:21:41,177 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [224825405] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,177 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,177 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,178 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1607101166]
[2025-04-28 21:21:41,178 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,178 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,178 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,179 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,179 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,179 INFO  L87              Difference]: Start difference. First operand 56 states and 90 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:41,230 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,230 INFO  L93              Difference]: Finished difference Result 60 states and 94 transitions.
[2025-04-28 21:21:41,231 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:41,231 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), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:41,232 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,233 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:41,233 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:41,234 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:41,234 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 1 mSDsluCounter, 160 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 247 SdHoareTripleChecker+Invalid, 11 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,235 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 247 Invalid, 11 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:41,236 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:41,242 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 56.
[2025-04-28 21:21:41,243 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 18 states have (on average 1.7777777777777777) internal successors, (32), 32 states have internal predecessors, (32), 27 states have call successors, (27), 8 states have call predecessors, (27), 10 states have return successors, (31), 17 states have call predecessors, (31), 27 states have call successors, (31)
[2025-04-28 21:21:41,248 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 90 transitions.
[2025-04-28 21:21:41,248 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 90 transitions. Word has length 16
[2025-04-28 21:21:41,248 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,248 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 90 transitions.
[2025-04-28 21:21:41,249 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), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:41,249 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 90 transitions.
[2025-04-28 21:21:41,250 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:41,250 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,251 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,251 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:41,253 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,254 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,254 INFO  L85        PathProgramCache]: Analyzing trace with hash -568943040, now seen corresponding path program 1 times
[2025-04-28 21:21:41,254 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,254 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [7543263]
[2025-04-28 21:21:41,254 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,254 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,261 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:41,266 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:41,266 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,267 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,354 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:41,355 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,355 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [7543263]
[2025-04-28 21:21:41,355 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [7543263] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,355 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,355 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,355 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [593223895]
[2025-04-28 21:21:41,355 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,356 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,356 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,356 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,356 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,357 INFO  L87              Difference]: Start difference. First operand 56 states and 90 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), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:41,403 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,404 INFO  L93              Difference]: Finished difference Result 56 states and 89 transitions.
[2025-04-28 21:21:41,404 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:41,404 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), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:41,405 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,406 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:41,406 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:41,406 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:41,407 INFO  L437           NwaCegarLoop]: 84 mSDtfsCounter, 0 mSDsluCounter, 156 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 240 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,408 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 240 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:41,409 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:41,414 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 53.
[2025-04-28 21:21:41,415 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 53 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 30 states have internal predecessors, (30), 26 states have call successors, (26), 8 states have call predecessors, (26), 9 states have return successors, (27), 16 states have call predecessors, (27), 26 states have call successors, (27)
[2025-04-28 21:21:41,416 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 83 transitions.
[2025-04-28 21:21:41,417 INFO  L79                 Accepts]: Start accepts. Automaton has 53 states and 83 transitions. Word has length 24
[2025-04-28 21:21:41,417 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,417 INFO  L485      AbstractCegarLoop]: Abstraction has 53 states and 83 transitions.
[2025-04-28 21:21:41,417 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), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:41,417 INFO  L278                IsEmpty]: Start isEmpty. Operand 53 states and 83 transitions.
[2025-04-28 21:21:41,418 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:41,419 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,419 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,419 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:41,419 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,420 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,420 INFO  L85        PathProgramCache]: Analyzing trace with hash 176646093, now seen corresponding path program 1 times
[2025-04-28 21:21:41,420 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,420 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2059722697]
[2025-04-28 21:21:41,420 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,420 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,426 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:41,435 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:41,436 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,436 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,684 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:41,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2059722697]
[2025-04-28 21:21:41,684 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2059722697] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,684 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,684 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:41,685 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1048858066]
[2025-04-28 21:21:41,685 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,685 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:41,685 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,685 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:41,686 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:41,686 INFO  L87              Difference]: Start difference. First operand 53 states and 83 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:41,855 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,855 INFO  L93              Difference]: Finished difference Result 59 states and 92 transitions.
[2025-04-28 21:21:41,859 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:41,859 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:41,860 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,861 INFO  L225             Difference]: With dead ends: 59
[2025-04-28 21:21:41,861 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:41,861 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:41,862 INFO  L437           NwaCegarLoop]: 79 mSDtfsCounter, 3 mSDsluCounter, 288 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 367 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,862 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 367 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:41,868 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:41,876 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 55.
[2025-04-28 21:21:41,876 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 55 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 31 states have internal predecessors, (31), 26 states have call successors, (26), 8 states have call predecessors, (26), 10 states have return successors, (30), 17 states have call predecessors, (30), 26 states have call successors, (30)
[2025-04-28 21:21:41,880 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 55 states to 55 states and 87 transitions.
[2025-04-28 21:21:41,880 INFO  L79                 Accepts]: Start accepts. Automaton has 55 states and 87 transitions. Word has length 24
[2025-04-28 21:21:41,881 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,881 INFO  L485      AbstractCegarLoop]: Abstraction has 55 states and 87 transitions.
[2025-04-28 21:21:41,881 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:41,881 INFO  L278                IsEmpty]: Start isEmpty. Operand 55 states and 87 transitions.
[2025-04-28 21:21:41,882 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:41,882 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,882 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,882 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:41,882 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,884 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,884 INFO  L85        PathProgramCache]: Analyzing trace with hash -1311925717, now seen corresponding path program 1 times
[2025-04-28 21:21:41,884 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,885 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1935498804]
[2025-04-28 21:21:41,885 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,885 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,891 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:41,901 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:41,905 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,905 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,013 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:42,014 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,014 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1935498804]
[2025-04-28 21:21:42,014 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1935498804] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,014 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,014 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:42,015 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [865592556]
[2025-04-28 21:21:42,015 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,015 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:42,015 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,016 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:42,016 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:42,017 INFO  L87              Difference]: Start difference. First operand 55 states and 87 transitions. Second operand  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 4 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:42,111 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,111 INFO  L93              Difference]: Finished difference Result 62 states and 96 transitions.
[2025-04-28 21:21:42,112 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:42,112 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 4 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:42,113 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,113 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:42,113 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:42,114 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,114 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 2 mSDsluCounter, 220 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 305 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,115 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 305 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:42,115 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:42,123 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 40.
[2025-04-28 21:21:42,123 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 14 states have (on average 1.5714285714285714) internal successors, (22), 22 states have internal predecessors, (22), 17 states have call successors, (17), 6 states have call predecessors, (17), 8 states have return successors, (21), 13 states have call predecessors, (21), 17 states have call successors, (21)
[2025-04-28 21:21:42,124 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 60 transitions.
[2025-04-28 21:21:42,124 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 60 transitions. Word has length 24
[2025-04-28 21:21:42,125 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,125 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 60 transitions.
[2025-04-28 21:21:42,125 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 4 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:42,125 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 60 transitions.
[2025-04-28 21:21:42,126 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:42,126 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,126 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,126 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:42,126 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,127 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,127 INFO  L85        PathProgramCache]: Analyzing trace with hash -1194710406, now seen corresponding path program 1 times
[2025-04-28 21:21:42,127 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,127 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [413309347]
[2025-04-28 21:21:42,127 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,127 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,132 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:42,138 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:42,139 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,139 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,343 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:42,344 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,344 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [413309347]
[2025-04-28 21:21:42,344 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [413309347] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,344 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [730037997]
[2025-04-28 21:21:42,344 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,344 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,348 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,353 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:42,355 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,400 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:42,422 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:42,422 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,422 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,425 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 35 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,432 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,694 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:42,695 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,550 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:43,550 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [730037997] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,551 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,551 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 12
[2025-04-28 21:21:43,551 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1887520163]
[2025-04-28 21:21:43,551 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,551 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:43,551 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,552 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:43,552 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=103, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:43,552 INFO  L87              Difference]: Start difference. First operand 40 states and 60 transitions. Second operand  has 12 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 12 states have internal predecessors, (17), 11 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 5 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:43,681 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,682 INFO  L93              Difference]: Finished difference Result 47 states and 69 transitions.
[2025-04-28 21:21:43,683 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:43,683 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 12 states have internal predecessors, (17), 11 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 5 states have call predecessors, (12), 11 states have call successors, (12) Word has length 24
[2025-04-28 21:21:43,683 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,684 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:43,684 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:43,684 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 43 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=36, Invalid=120, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:43,685 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 5 mSDsluCounter, 342 mSDsCounter, 0 mSdLazyCounter, 62 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 400 SdHoareTripleChecker+Invalid, 67 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 62 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,685 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 400 Invalid, 67 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 62 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,686 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:43,692 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 43.
[2025-04-28 21:21:43,692 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 43 states, 15 states have (on average 1.5333333333333334) internal successors, (23), 23 states have internal predecessors, (23), 18 states have call successors, (18), 6 states have call predecessors, (18), 9 states have return successors, (23), 15 states have call predecessors, (23), 18 states have call successors, (23)
[2025-04-28 21:21:43,695 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 43 states to 43 states and 64 transitions.
[2025-04-28 21:21:43,695 INFO  L79                 Accepts]: Start accepts. Automaton has 43 states and 64 transitions. Word has length 24
[2025-04-28 21:21:43,695 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,695 INFO  L485      AbstractCegarLoop]: Abstraction has 43 states and 64 transitions.
[2025-04-28 21:21:43,695 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 12 states have internal predecessors, (17), 11 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (12), 5 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:43,696 INFO  L278                IsEmpty]: Start isEmpty. Operand 43 states and 64 transitions.
[2025-04-28 21:21:43,696 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:43,696 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,699 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,706 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:43,900 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,900 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,901 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,901 INFO  L85        PathProgramCache]: Analyzing trace with hash 515546023, now seen corresponding path program 1 times
[2025-04-28 21:21:43,901 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,901 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [424155430]
[2025-04-28 21:21:43,902 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,902 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,907 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:43,912 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:43,912 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,913 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,961 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,961 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,962 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [424155430]
[2025-04-28 21:21:43,962 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [424155430] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,962 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,962 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:43,962 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1027277186]
[2025-04-28 21:21:43,963 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,963 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,963 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,964 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,964 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,964 INFO  L87              Difference]: Start difference. First operand 43 states and 64 transitions. Second operand  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:43,985 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,985 INFO  L93              Difference]: Finished difference Result 45 states and 66 transitions.
[2025-04-28 21:21:43,986 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:43,986 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:43,987 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,987 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:43,987 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:43,988 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:43,989 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 1 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 8 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 150 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 8 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,990 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 150 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 8 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:43,991 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:43,996 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 43.
[2025-04-28 21:21:43,997 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 43 states, 15 states have (on average 1.5333333333333334) internal successors, (23), 23 states have internal predecessors, (23), 18 states have call successors, (18), 6 states have call predecessors, (18), 9 states have return successors, (23), 15 states have call predecessors, (23), 18 states have call successors, (23)
[2025-04-28 21:21:43,998 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 43 states to 43 states and 64 transitions.
[2025-04-28 21:21:43,998 INFO  L79                 Accepts]: Start accepts. Automaton has 43 states and 64 transitions. Word has length 24
[2025-04-28 21:21:43,998 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,998 INFO  L485      AbstractCegarLoop]: Abstraction has 43 states and 64 transitions.
[2025-04-28 21:21:43,998 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:43,998 INFO  L278                IsEmpty]: Start isEmpty. Operand 43 states and 64 transitions.
[2025-04-28 21:21:43,999 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:43,999 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,999 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,999 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:44,000 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,000 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,000 INFO  L85        PathProgramCache]: Analyzing trace with hash 975013651, now seen corresponding path program 1 times
[2025-04-28 21:21:44,000 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,000 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1941038292]
[2025-04-28 21:21:44,000 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,000 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,005 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:44,011 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:44,011 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,011 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,102 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:44,103 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1941038292]
[2025-04-28 21:21:44,103 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1941038292] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,103 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,103 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:44,103 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2111852480]
[2025-04-28 21:21:44,103 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,103 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:44,103 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,104 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:44,104 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,104 INFO  L87              Difference]: Start difference. First operand 43 states and 64 transitions. Second operand  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:44,183 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,183 INFO  L93              Difference]: Finished difference Result 47 states and 68 transitions.
[2025-04-28 21:21:44,184 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:44,184 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:21:44,184 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,185 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:44,185 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:44,185 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:44,186 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 2 mSDsluCounter, 195 mSDsCounter, 0 mSdLazyCounter, 42 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 252 SdHoareTripleChecker+Invalid, 42 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 42 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,186 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 252 Invalid, 42 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 42 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:44,187 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:44,193 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 41.
[2025-04-28 21:21:44,193 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 14 states have (on average 1.5714285714285714) internal successors, (22), 22 states have internal predecessors, (22), 18 states have call successors, (18), 6 states have call predecessors, (18), 8 states have return successors, (20), 14 states have call predecessors, (20), 18 states have call successors, (20)
[2025-04-28 21:21:44,198 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 60 transitions.
[2025-04-28 21:21:44,198 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 60 transitions. Word has length 32
[2025-04-28 21:21:44,198 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,198 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 60 transitions.
[2025-04-28 21:21:44,199 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:44,199 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 60 transitions.
[2025-04-28 21:21:44,199 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:44,199 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,200 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,200 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:44,200 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,200 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,200 INFO  L85        PathProgramCache]: Analyzing trace with hash -1505006016, now seen corresponding path program 1 times
[2025-04-28 21:21:44,200 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,200 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1715484766]
[2025-04-28 21:21:44,201 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,201 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,211 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:44,224 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:44,224 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,224 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,503 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:44,503 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,503 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1715484766]
[2025-04-28 21:21:44,504 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1715484766] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,504 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [730935360]
[2025-04-28 21:21:44,504 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,504 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,506 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,509 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:44,512 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,549 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:44,571 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:44,571 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,573 INFO  L256         TraceCheckSpWp]: Trace formula consists of 125 conjuncts, 41 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,576 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,050 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:45,050 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,076 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:47,077 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [730935360] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,077 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,077 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:47,077 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1104260211]
[2025-04-28 21:21:47,077 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,078 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:47,081 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,081 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:47,082 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=226, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:47,082 INFO  L87              Difference]: Start difference. First operand 41 states and 60 transitions. Second operand  has 17 states, 8 states have (on average 2.875) internal successors, (23), 17 states have internal predecessors, (23), 13 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (17), 10 states have call predecessors, (17), 13 states have call successors, (17)
[2025-04-28 21:21:47,426 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,426 INFO  L93              Difference]: Finished difference Result 52 states and 74 transitions.
[2025-04-28 21:21:47,427 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:47,427 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.875) internal successors, (23), 17 states have internal predecessors, (23), 13 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (17), 10 states have call predecessors, (17), 13 states have call successors, (17) Word has length 32
[2025-04-28 21:21:47,427 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,428 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:47,428 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:47,428 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 55 SyntacticMatches, 1 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 49 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=62, Invalid=280, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:47,429 INFO  L437           NwaCegarLoop]: 55 mSDtfsCounter, 9 mSDsluCounter, 513 mSDsCounter, 0 mSdLazyCounter, 144 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 568 SdHoareTripleChecker+Invalid, 151 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 144 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,429 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 568 Invalid, 151 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 144 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:47,430 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:47,434 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 43.
[2025-04-28 21:21:47,434 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 43 states, 15 states have (on average 1.5333333333333334) internal successors, (23), 23 states have internal predecessors, (23), 18 states have call successors, (18), 6 states have call predecessors, (18), 9 states have return successors, (23), 15 states have call predecessors, (23), 18 states have call successors, (23)
[2025-04-28 21:21:47,435 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 43 states to 43 states and 64 transitions.
[2025-04-28 21:21:47,435 INFO  L79                 Accepts]: Start accepts. Automaton has 43 states and 64 transitions. Word has length 32
[2025-04-28 21:21:47,435 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,435 INFO  L485      AbstractCegarLoop]: Abstraction has 43 states and 64 transitions.
[2025-04-28 21:21:47,435 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.875) internal successors, (23), 17 states have internal predecessors, (23), 13 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (17), 10 states have call predecessors, (17), 13 states have call successors, (17)
[2025-04-28 21:21:47,435 INFO  L278                IsEmpty]: Start isEmpty. Operand 43 states and 64 transitions.
[2025-04-28 21:21:47,436 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:47,436 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,436 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,441 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:47,641 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,641 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,642 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,642 INFO  L85        PathProgramCache]: Analyzing trace with hash 1401600813, now seen corresponding path program 2 times
[2025-04-28 21:21:47,642 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,642 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1960285536]
[2025-04-28 21:21:47,642 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,643 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,648 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:47,662 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:47,662 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,663 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,879 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:47,879 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,880 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1960285536]
[2025-04-28 21:21:47,880 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1960285536] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,880 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1707660321]
[2025-04-28 21:21:47,880 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,882 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,884 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,887 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:47,890 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,934 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:47,958 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:47,958 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,958 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,964 INFO  L256         TraceCheckSpWp]: Trace formula consists of 138 conjuncts, 51 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,966 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,146 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:48,147 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,389 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:49,389 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1707660321] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,389 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,389 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 7, 8] total 15
[2025-04-28 21:21:49,389 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [213155848]
[2025-04-28 21:21:49,389 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,390 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:49,390 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,390 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:49,391 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=172, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:49,391 INFO  L87              Difference]: Start difference. First operand 43 states and 64 transitions. Second operand  has 15 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 15 states have internal predecessors, (19), 14 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 6 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:49,567 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,567 INFO  L93              Difference]: Finished difference Result 53 states and 76 transitions.
[2025-04-28 21:21:49,567 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:49,568 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 15 states have internal predecessors, (19), 14 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 6 states have call predecessors, (16), 14 states have call successors, (16) Word has length 32
[2025-04-28 21:21:49,568 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,568 INFO  L225             Difference]: With dead ends: 53
[2025-04-28 21:21:49,568 INFO  L226             Difference]: Without dead ends: 53
[2025-04-28 21:21:49,569 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 58 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 27 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=56, Invalid=216, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:49,569 INFO  L437           NwaCegarLoop]: 60 mSDtfsCounter, 7 mSDsluCounter, 443 mSDsCounter, 0 mSdLazyCounter, 85 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 503 SdHoareTripleChecker+Invalid, 94 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 85 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,570 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 503 Invalid, 94 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 85 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,570 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 53 states.
[2025-04-28 21:21:49,574 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 53 to 46.
[2025-04-28 21:21:49,575 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 16 states have (on average 1.5) internal successors, (24), 24 states have internal predecessors, (24), 19 states have call successors, (19), 6 states have call predecessors, (19), 10 states have return successors, (25), 17 states have call predecessors, (25), 19 states have call successors, (25)
[2025-04-28 21:21:49,575 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 68 transitions.
[2025-04-28 21:21:49,575 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 68 transitions. Word has length 32
[2025-04-28 21:21:49,576 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,576 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 68 transitions.
[2025-04-28 21:21:49,576 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 15 states have internal predecessors, (19), 14 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 6 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:49,576 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 68 transitions.
[2025-04-28 21:21:49,577 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:49,577 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,577 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,582 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:49,781 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,781 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,781 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,781 INFO  L85        PathProgramCache]: Analyzing trace with hash 1914361498, now seen corresponding path program 1 times
[2025-04-28 21:21:49,781 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,781 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1133169266]
[2025-04-28 21:21:49,781 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,782 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,786 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:49,791 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:49,791 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,791 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,855 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:49,855 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,855 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1133169266]
[2025-04-28 21:21:49,855 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1133169266] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,855 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,855 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:49,856 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1947664751]
[2025-04-28 21:21:49,856 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,856 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:49,856 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,857 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:49,857 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:49,857 INFO  L87              Difference]: Start difference. First operand 46 states and 68 transitions. Second operand  has 5 states, 3 states have (on average 4.333333333333333) internal successors, (13), 5 states have internal predecessors, (13), 4 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:49,904 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,904 INFO  L93              Difference]: Finished difference Result 55 states and 78 transitions.
[2025-04-28 21:21:49,905 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:49,905 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 4.333333333333333) internal successors, (13), 5 states have internal predecessors, (13), 4 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:21:49,905 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,906 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:49,906 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:49,906 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:49,906 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 3 mSDsluCounter, 139 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 193 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,907 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 193 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:49,907 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:49,910 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 44.
[2025-04-28 21:21:49,910 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 16 states have (on average 1.4375) internal successors, (23), 23 states have internal predecessors, (23), 17 states have call successors, (17), 6 states have call predecessors, (17), 10 states have return successors, (22), 16 states have call predecessors, (22), 17 states have call successors, (22)
[2025-04-28 21:21:49,911 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 62 transitions.
[2025-04-28 21:21:49,911 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 62 transitions. Word has length 32
[2025-04-28 21:21:49,911 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,911 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 62 transitions.
[2025-04-28 21:21:49,911 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 4.333333333333333) internal successors, (13), 5 states have internal predecessors, (13), 4 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:49,912 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 62 transitions.
[2025-04-28 21:21:49,912 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:49,912 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,912 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,912 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:49,913 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,913 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,913 INFO  L85        PathProgramCache]: Analyzing trace with hash 1190328736, now seen corresponding path program 3 times
[2025-04-28 21:21:49,913 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,913 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1618807960]
[2025-04-28 21:21:49,913 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:49,913 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,918 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 40 statements into 4 equivalence classes.
[2025-04-28 21:21:49,930 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:49,930 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:49,930 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,310 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:50,310 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,310 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1618807960]
[2025-04-28 21:21:50,310 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1618807960] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,310 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [41684784]
[2025-04-28 21:21:50,310 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:50,310 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,313 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,315 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:50,320 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,364 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 40 statements into 4 equivalence classes.
[2025-04-28 21:21:50,393 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:50,393 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:50,393 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,396 INFO  L256         TraceCheckSpWp]: Trace formula consists of 178 conjuncts, 69 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,399 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,087 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:51,087 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,508 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:54,508 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [41684784] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,508 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,508 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 27
[2025-04-28 21:21:54,509 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [339855382]
[2025-04-28 21:21:54,509 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,509 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:21:54,509 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,510 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:21:54,510 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=82, Invalid=620, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:54,511 INFO  L87              Difference]: Start difference. First operand 44 states and 62 transitions. Second operand  has 27 states, 12 states have (on average 2.5833333333333335) internal successors, (31), 27 states have internal predecessors, (31), 22 states have call successors, (23), 1 states have call predecessors, (23), 12 states have return successors, (23), 10 states have call predecessors, (23), 22 states have call successors, (23)
[2025-04-28 21:21:55,321 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,321 INFO  L93              Difference]: Finished difference Result 66 states and 98 transitions.
[2025-04-28 21:21:55,322 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:55,322 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 12 states have (on average 2.5833333333333335) internal successors, (31), 27 states have internal predecessors, (31), 22 states have call successors, (23), 1 states have call predecessors, (23), 12 states have return successors, (23), 10 states have call predecessors, (23), 22 states have call successors, (23) Word has length 40
[2025-04-28 21:21:55,322 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,324 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:21:55,324 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:55,324 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 63 SyntacticMatches, 3 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 177 ImplicationChecksByTransitivity, 1.4s TimeCoverageRelationStatistics Valid=159, Invalid=833, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:55,325 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 13 mSDsluCounter, 621 mSDsCounter, 0 mSdLazyCounter, 310 mSolverCounterSat, 39 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 670 SdHoareTripleChecker+Invalid, 349 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 39 IncrementalHoareTripleChecker+Valid, 310 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,325 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 670 Invalid, 349 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [39 Valid, 310 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:55,326 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:55,333 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:55,337 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.411764705882353) internal successors, (24), 24 states have internal predecessors, (24), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (29), 16 states have call predecessors, (29), 17 states have call successors, (29)
[2025-04-28 21:21:55,337 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 70 transitions.
[2025-04-28 21:21:55,337 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 70 transitions. Word has length 40
[2025-04-28 21:21:55,338 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,338 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 70 transitions.
[2025-04-28 21:21:55,338 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 12 states have (on average 2.5833333333333335) internal successors, (31), 27 states have internal predecessors, (31), 22 states have call successors, (23), 1 states have call predecessors, (23), 12 states have return successors, (23), 10 states have call predecessors, (23), 22 states have call successors, (23)
[2025-04-28 21:21:55,338 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 70 transitions.
[2025-04-28 21:21:55,339 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:55,339 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,339 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,344 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:55,539 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-04-28 21:21:55,540 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,540 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,540 INFO  L85        PathProgramCache]: Analyzing trace with hash -1881489146, now seen corresponding path program 1 times
[2025-04-28 21:21:55,540 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,540 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [310059649]
[2025-04-28 21:21:55,540 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,540 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,544 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:55,550 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:55,550 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,550 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,586 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:55,586 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,586 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [310059649]
[2025-04-28 21:21:55,586 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [310059649] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,586 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1887355258]
[2025-04-28 21:21:55,586 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,586 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,589 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,591 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:55,596 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,647 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:55,668 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:55,668 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,668 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,669 INFO  L256         TraceCheckSpWp]: Trace formula consists of 151 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,671 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,768 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:55,768 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,518 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:56,518 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1887355258] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,518 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,518 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 8, 8] total 12
[2025-04-28 21:21:56,519 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [463067504]
[2025-04-28 21:21:56,519 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,519 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:56,521 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,521 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:56,521 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=105, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:56,522 INFO  L87              Difference]: Start difference. First operand 46 states and 70 transitions. Second operand  has 12 states, 6 states have (on average 4.333333333333333) internal successors, (26), 12 states have internal predecessors, (26), 10 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (21), 7 states have call predecessors, (21), 10 states have call successors, (21)
[2025-04-28 21:21:56,670 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,670 INFO  L93              Difference]: Finished difference Result 55 states and 82 transitions.
[2025-04-28 21:21:56,671 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:56,671 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 4.333333333333333) internal successors, (26), 12 states have internal predecessors, (26), 10 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (21), 7 states have call predecessors, (21), 10 states have call successors, (21) Word has length 40
[2025-04-28 21:21:56,671 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,672 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:56,672 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:56,672 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 85 GetRequests, 71 SyntacticMatches, 2 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=38, Invalid=144, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:56,672 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 5 mSDsluCounter, 340 mSDsCounter, 0 mSdLazyCounter, 121 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 393 SdHoareTripleChecker+Invalid, 123 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 121 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,674 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 393 Invalid, 123 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 121 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,674 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:56,679 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 46.
[2025-04-28 21:21:56,680 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.411764705882353) internal successors, (24), 24 states have internal predecessors, (24), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (29), 15 states have call predecessors, (29), 17 states have call successors, (29)
[2025-04-28 21:21:56,680 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 70 transitions.
[2025-04-28 21:21:56,680 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 70 transitions. Word has length 40
[2025-04-28 21:21:56,680 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,681 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 70 transitions.
[2025-04-28 21:21:56,681 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 4.333333333333333) internal successors, (26), 12 states have internal predecessors, (26), 10 states have call successors, (20), 1 states have call predecessors, (20), 6 states have return successors, (21), 7 states have call predecessors, (21), 10 states have call successors, (21)
[2025-04-28 21:21:56,681 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 70 transitions.
[2025-04-28 21:21:56,681 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:56,682 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,682 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,686 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:56,886 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,886 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,887 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,887 INFO  L85        PathProgramCache]: Analyzing trace with hash 1916260979, now seen corresponding path program 2 times
[2025-04-28 21:21:56,887 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,887 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1576258586]
[2025-04-28 21:21:56,887 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,887 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,891 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 40 statements into 2 equivalence classes.
[2025-04-28 21:21:56,901 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:56,901 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:56,901 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,228 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:57,228 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,228 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1576258586]
[2025-04-28 21:21:57,228 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1576258586] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,228 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [942632560]
[2025-04-28 21:21:57,228 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:57,229 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,231 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,233 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:57,236 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,297 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 40 statements into 2 equivalence classes.
[2025-04-28 21:21:57,325 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:57,325 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:57,325 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,327 INFO  L256         TraceCheckSpWp]: Trace formula consists of 165 conjuncts, 57 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,330 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,877 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:57,877 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:00,537 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:22:00,537 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [942632560] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,537 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,537 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:00,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1901324482]
[2025-04-28 21:22:00,537 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,538 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:00,538 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,539 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:00,539 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=399, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:00,540 INFO  L87              Difference]: Start difference. First operand 46 states and 70 transitions. Second operand  has 22 states, 10 states have (on average 2.8) internal successors, (28), 22 states have internal predecessors, (28), 18 states have call successors, (22), 1 states have call predecessors, (22), 10 states have return successors, (22), 12 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:22:00,923 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,923 INFO  L93              Difference]: Finished difference Result 58 states and 87 transitions.
[2025-04-28 21:22:00,924 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:00,924 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 22 states have internal predecessors, (28), 18 states have call successors, (22), 1 states have call predecessors, (22), 10 states have return successors, (22), 12 states have call predecessors, (22), 18 states have call successors, (22) Word has length 40
[2025-04-28 21:22:00,925 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,925 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:22:00,925 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:22:00,926 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 92 GetRequests, 67 SyntacticMatches, 2 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 107 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=93, Invalid=507, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:22:00,926 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 11 mSDsluCounter, 513 mSDsCounter, 0 mSdLazyCounter, 143 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 566 SdHoareTripleChecker+Invalid, 153 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 143 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,927 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 566 Invalid, 153 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 143 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:00,927 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:22:00,931 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 48.
[2025-04-28 21:22:00,932 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 18 states have (on average 1.3888888888888888) internal successors, (25), 25 states have internal predecessors, (25), 17 states have call successors, (17), 6 states have call predecessors, (17), 12 states have return successors, (31), 16 states have call predecessors, (31), 17 states have call successors, (31)
[2025-04-28 21:22:00,932 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 73 transitions.
[2025-04-28 21:22:00,933 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 73 transitions. Word has length 40
[2025-04-28 21:22:00,933 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,934 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 73 transitions.
[2025-04-28 21:22:00,934 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 22 states have internal predecessors, (28), 18 states have call successors, (22), 1 states have call predecessors, (22), 10 states have return successors, (22), 12 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:22:00,934 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 73 transitions.
[2025-04-28 21:22:00,934 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:22:00,934 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,935 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,940 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:01,135 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable16
[2025-04-28 21:22:01,135 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,135 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,136 INFO  L85        PathProgramCache]: Analyzing trace with hash 601165252, now seen corresponding path program 1 times
[2025-04-28 21:22:01,136 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,136 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1508113059]
[2025-04-28 21:22:01,136 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,136 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,140 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:22:01,151 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:01,151 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,151 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,447 INFO  L134       CoverageAnalysis]: Checked inductivity of 54 backedges. 6 proven. 20 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:22:01,448 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,448 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1508113059]
[2025-04-28 21:22:01,448 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1508113059] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,448 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [791326604]
[2025-04-28 21:22:01,448 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,448 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,451 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,453 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:01,456 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,518 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:22:01,543 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:01,543 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,543 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,545 INFO  L256         TraceCheckSpWp]: Trace formula consists of 193 conjuncts, 67 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,547 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,812 INFO  L134       CoverageAnalysis]: Checked inductivity of 54 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 39 trivial. 0 not checked.
[2025-04-28 21:22:01,812 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:03,531 INFO  L134       CoverageAnalysis]: Checked inductivity of 54 backedges. 0 proven. 18 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:22:03,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [791326604] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:03,532 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:03,532 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 8, 10] total 22
[2025-04-28 21:22:03,532 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1783417862]
[2025-04-28 21:22:03,532 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,532 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:03,532 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,533 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:03,533 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=55, Invalid=407, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:03,533 INFO  L87              Difference]: Start difference. First operand 48 states and 73 transitions. Second operand  has 22 states, 11 states have (on average 2.5454545454545454) internal successors, (28), 21 states have internal predecessors, (28), 19 states have call successors, (21), 1 states have call predecessors, (21), 11 states have return successors, (23), 11 states have call predecessors, (23), 19 states have call successors, (23)
[2025-04-28 21:22:04,195 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,195 INFO  L93              Difference]: Finished difference Result 76 states and 115 transitions.
[2025-04-28 21:22:04,196 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:04,196 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.5454545454545454) internal successors, (28), 21 states have internal predecessors, (28), 19 states have call successors, (21), 1 states have call predecessors, (21), 11 states have return successors, (23), 11 states have call predecessors, (23), 19 states have call successors, (23) Word has length 44
[2025-04-28 21:22:04,197 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,197 INFO  L225             Difference]: With dead ends: 76
[2025-04-28 21:22:04,197 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:22:04,198 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 106 GetRequests, 79 SyntacticMatches, 0 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 75 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=152, Invalid=660, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:22:04,198 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 30 mSDsluCounter, 700 mSDsCounter, 0 mSdLazyCounter, 340 mSolverCounterSat, 74 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 37 SdHoareTripleChecker+Valid, 749 SdHoareTripleChecker+Invalid, 414 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 74 IncrementalHoareTripleChecker+Valid, 340 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,198 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [37 Valid, 749 Invalid, 414 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [74 Valid, 340 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:04,199 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:22:04,203 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 57.
[2025-04-28 21:22:04,204 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 21 states have (on average 1.3333333333333333) internal successors, (28), 28 states have internal predecessors, (28), 20 states have call successors, (20), 6 states have call predecessors, (20), 15 states have return successors, (37), 22 states have call predecessors, (37), 20 states have call successors, (37)
[2025-04-28 21:22:04,204 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 85 transitions.
[2025-04-28 21:22:04,205 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 85 transitions. Word has length 44
[2025-04-28 21:22:04,205 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,205 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 85 transitions.
[2025-04-28 21:22:04,205 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.5454545454545454) internal successors, (28), 21 states have internal predecessors, (28), 19 states have call successors, (21), 1 states have call predecessors, (21), 11 states have return successors, (23), 11 states have call predecessors, (23), 19 states have call successors, (23)
[2025-04-28 21:22:04,205 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 85 transitions.
[2025-04-28 21:22:04,206 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:22:04,206 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,206 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 4, 3, 3, 3, 3, 3, 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:04,212 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:22:04,410 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:22:04,410 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,411 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,411 INFO  L85        PathProgramCache]: Analyzing trace with hash 1144996966, now seen corresponding path program 3 times
[2025-04-28 21:22:04,411 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,411 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1447876433]
[2025-04-28 21:22:04,411 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:04,411 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,416 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 4 equivalence classes.
[2025-04-28 21:22:04,427 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:22:04,427 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:22:04,427 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,805 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 4 proven. 20 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:04,806 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,806 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1447876433]
[2025-04-28 21:22:04,806 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1447876433] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,806 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2025071695]
[2025-04-28 21:22:04,806 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:04,806 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,809 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,811 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,816 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,889 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 4 equivalence classes.
[2025-04-28 21:22:04,922 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:22:04,922 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:22:04,922 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,925 INFO  L256         TraceCheckSpWp]: Trace formula consists of 205 conjuncts, 74 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,928 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:05,622 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:05,623 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:10,486 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:10,486 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2025071695] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:10,486 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:10,486 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 14, 14] total 29
[2025-04-28 21:22:10,487 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1271478486]
[2025-04-28 21:22:10,487 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:10,487 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 29 states
[2025-04-28 21:22:10,487 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:10,488 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 29 interpolants.
[2025-04-28 21:22:10,488 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=88, Invalid=724, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:22:10,488 INFO  L87              Difference]: Start difference. First operand 57 states and 85 transitions. Second operand  has 29 states, 12 states have (on average 2.8333333333333335) internal successors, (34), 26 states have internal predecessors, (34), 24 states have call successors, (25), 1 states have call predecessors, (25), 12 states have return successors, (26), 12 states have call predecessors, (26), 24 states have call successors, (26)
