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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:47,340 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:47,408 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9c2c5e8b-701c-4ba8-88a1-a933a699a8e5/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:47,417 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:47,418 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:47,450 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:47,452 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:47,452 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:47,453 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:47,454 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:47,455 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:47,455 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:47,455 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:47,456 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:47,456 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:47,456 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:47,456 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:47,457 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:47,457 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:47,457 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:47,457 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:47,457 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:47,457 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:47,457 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:47,458 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:47,458 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:47,459 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:47,795 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:47,803 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:47,806 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:47,807 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:47,807 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:47,809 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9c2c5e8b-701c-4ba8-88a1-a933a699a8e5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-029.smt2
[2025-04-28 21:21:47,810 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:47,814 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:48,347 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9c2c5e8b-701c-4ba8-88a1-a933a699a8e5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-029.smt2
[2025-04-28 21:21:48,350 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:48,353 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:48,354 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:48,354 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:48,355 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:48,359 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,421 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48 Unit
[2025-04-28 21:21:48,421 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:48,422 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:48,422 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:48,422 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:48,440 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,440 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,473 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,473 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,480 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,482 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,488 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,490 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,495 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,514 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:48,515 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:48,515 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:48,515 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:48,516 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,521 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:48,536 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,551 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:48,557 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:48,571 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:48,571 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:48,572 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:48,572 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:48,572 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:48,572 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:48,572 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcmainStart__sem given in one single declaration
[2025-04-28 21:21:48,572 INFO  L130     BoogieDeclarations]: Found specification of procedure funcmainStart__sem
[2025-04-28 21:21:48,572 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcmainStart__sem
[2025-04-28 21:21:48,572 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:48,572 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:48,573 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:48,574 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStartBool__sem given in one single declaration
[2025-04-28 21:21:48,574 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStartBool__sem
[2025-04-28 21:21:48,574 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStartBool__sem
[2025-04-28 21:21:48,575 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcmainStart__syn given in one single declaration
[2025-04-28 21:21:48,575 INFO  L130     BoogieDeclarations]: Found specification of procedure funcmainStart__syn
[2025-04-28 21:21:48,575 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcmainStart__syn
[2025-04-28 21:21:48,575 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:48,575 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:48,575 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:48,575 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStartBool__syn given in one single declaration
[2025-04-28 21:21:48,575 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStartBool__syn
[2025-04-28 21:21:48,576 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStartBool__syn
[2025-04-28 21:21:48,577 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:48,577 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:48,577 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:48,752 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:48,755 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:49,202 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:49,203 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:49,228 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:49,232 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:49,233 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:49 BoogieIcfgContainer
[2025-04-28 21:21:49,233 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:49,235 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:49,235 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:49,241 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:49,242 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:48" (1/3) ...
[2025-04-28 21:21:49,243 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7d6c1a0a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:49, skipping insertion in model container
[2025-04-28 21:21:49,247 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (2/3) ...
[2025-04-28 21:21:49,247 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7d6c1a0a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:49, skipping insertion in model container
[2025-04-28 21:21:49,247 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:49" (3/3) ...
[2025-04-28 21:21:49,248 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:49,264 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:49,266 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 9 procedures, 57 locations, 148 edges, 9 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:49,337 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:49,354 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;@61523567, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:49,355 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:49,360 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 57 states, 17 states have (on average 3.411764705882353) internal successors, (58), 28 states have internal predecessors, (58), 30 states have call successors, (30), 8 states have call predecessors, (30), 8 states have return successors, (30), 22 states have call predecessors, (30), 30 states have call successors, (30)
[2025-04-28 21:21:49,376 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:49,376 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,377 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:49,377 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,384 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,384 INFO  L85        PathProgramCache]: Analyzing trace with hash 1877469172, now seen corresponding path program 1 times
[2025-04-28 21:21:49,392 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,393 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2083103026]
[2025-04-28 21:21:49,393 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,393 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,450 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:49,562 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,563 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,563 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,153 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:50,154 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,154 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2083103026]
[2025-04-28 21:21:50,155 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2083103026] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,155 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,158 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:50,160 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [412510153]
[2025-04-28 21:21:50,164 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,168 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:50,168 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,207 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:50,208 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,210 INFO  L87              Difference]: Start difference. First operand  has 57 states, 17 states have (on average 3.411764705882353) internal successors, (58), 28 states have internal predecessors, (58), 30 states have call successors, (30), 8 states have call predecessors, (30), 8 states have return successors, (30), 22 states have call predecessors, (30), 30 states have call successors, (30) Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,594 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,595 INFO  L93              Difference]: Finished difference Result 59 states and 125 transitions.
[2025-04-28 21:21:50,597 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:50,598 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:50,599 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,608 INFO  L225             Difference]: With dead ends: 59
[2025-04-28 21:21:50,608 INFO  L226             Difference]: Without dead ends: 57
[2025-04-28 21:21:50,613 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:50,617 INFO  L437           NwaCegarLoop]: 108 mSDtfsCounter, 3 mSDsluCounter, 399 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 507 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,618 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 507 Invalid, 65 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:50,634 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 57 states.
[2025-04-28 21:21:50,670 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 57 to 57.
[2025-04-28 21:21:50,675 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:50,686 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:50,689 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:50,691 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,692 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:50,692 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,692 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:50,696 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:50,697 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,697 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:50,697 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:50,698 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,699 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,699 INFO  L85        PathProgramCache]: Analyzing trace with hash -620546765, now seen corresponding path program 1 times
[2025-04-28 21:21:50,699 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,699 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1089202859]
[2025-04-28 21:21:50,699 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,699 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,721 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:50,765 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:50,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,767 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,097 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:51,098 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,098 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1089202859]
[2025-04-28 21:21:51,098 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1089202859] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,098 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,098 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:51,098 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1414967936]
[2025-04-28 21:21:51,099 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,100 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:51,100 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,100 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:51,101 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:51,101 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:51,341 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,341 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:51,343 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:51,343 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:51,343 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,346 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:51,346 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:51,346 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:51,350 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,350 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,351 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:51,360 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:51,360 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:51,362 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:51,363 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:51,363 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,363 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:51,363 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:51,363 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:51,365 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:51,366 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,366 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:51,366 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:51,366 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,367 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,367 INFO  L85        PathProgramCache]: Analyzing trace with hash 1091415152, now seen corresponding path program 1 times
[2025-04-28 21:21:51,367 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,367 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1242839771]
[2025-04-28 21:21:51,367 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,367 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,382 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:51,398 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:51,398 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,398 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,615 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:51,615 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,616 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1242839771]
[2025-04-28 21:21:51,616 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1242839771] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,616 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,616 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:51,616 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1309995668]
[2025-04-28 21:21:51,616 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,616 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:51,617 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,617 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:51,617 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:51,617 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:51,818 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,820 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:51,820 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:51,821 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:51,821 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,825 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:51,825 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:51,826 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:51,826 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,827 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:51,827 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:51,839 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:51,841 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:51,843 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:51,846 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:51,846 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,847 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:51,847 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:51,847 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:51,848 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:51,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,849 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:51,849 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:51,851 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,851 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,852 INFO  L85        PathProgramCache]: Analyzing trace with hash -1406600785, now seen corresponding path program 1 times
[2025-04-28 21:21:51,852 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,852 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1050693171]
[2025-04-28 21:21:51,852 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,852 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,871 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:51,890 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:51,890 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,890 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,138 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:52,138 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,138 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1050693171]
[2025-04-28 21:21:52,138 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1050693171] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,138 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,138 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:52,138 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [604245482]
[2025-04-28 21:21:52,139 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,139 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:52,139 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,139 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:52,140 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,140 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:52,353 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,353 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:52,354 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:52,354 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:52,354 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,356 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:52,356 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:52,356 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:52,357 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,361 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,361 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:52,374 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:52,374 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:52,376 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:52,376 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:52,376 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,376 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:52,376 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:52,377 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:52,381 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:52,381 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,381 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:52,382 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:52,382 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,382 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,382 INFO  L85        PathProgramCache]: Analyzing trace with hash 305361132, now seen corresponding path program 1 times
[2025-04-28 21:21:52,382 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,382 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1466358403]
[2025-04-28 21:21:52,382 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,383 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,396 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:52,415 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:52,415 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,415 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,602 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:52,602 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,603 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1466358403]
[2025-04-28 21:21:52,603 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1466358403] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,603 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,603 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:52,603 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1944768726]
[2025-04-28 21:21:52,603 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,603 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:52,603 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,604 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:52,604 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,604 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:52,834 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,834 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:52,835 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:52,835 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:52,835 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,839 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:52,839 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:52,839 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:52,840 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,843 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,843 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:52,858 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:52,858 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:52,860 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:52,860 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:52,860 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,860 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:52,861 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:52,861 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:52,866 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:52,866 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,866 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:52,866 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:52,866 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,867 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,867 INFO  L85        PathProgramCache]: Analyzing trace with hash 2102312491, now seen corresponding path program 1 times
[2025-04-28 21:21:52,867 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,867 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1271683405]
[2025-04-28 21:21:52,867 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,867 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,887 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:52,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:52,901 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,901 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,125 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:53,126 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,126 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1271683405]
[2025-04-28 21:21:53,126 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1271683405] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,126 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,126 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:53,126 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1750891895]
[2025-04-28 21:21:53,126 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:53,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,127 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:53,127 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,128 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:53,337 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,337 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:53,339 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:53,339 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:53,339 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,341 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:53,341 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:53,341 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:53,342 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,342 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:53,346 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:53,355 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:53,359 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:53,360 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:53,361 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:53,361 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,361 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:53,361 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:53,361 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:53,362 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:53,365 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,365 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:53,365 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:53,365 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,365 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,366 INFO  L85        PathProgramCache]: Analyzing trace with hash -480692888, now seen corresponding path program 1 times
[2025-04-28 21:21:53,366 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,366 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [273832686]
[2025-04-28 21:21:53,366 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,366 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,378 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:53,389 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:53,390 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,390 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,536 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:53,536 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,536 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [273832686]
[2025-04-28 21:21:53,536 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [273832686] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,536 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,536 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:53,536 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [47231438]
[2025-04-28 21:21:53,536 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,537 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:53,537 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,537 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:53,538 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,538 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:53,721 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,721 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:53,722 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:53,722 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:53,723 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,725 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:53,726 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:53,727 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:53,727 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,729 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:53,730 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:53,739 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:53,742 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:53,744 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:53,744 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:53,744 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,744 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:53,747 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:53,747 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:53,748 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:53,748 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,748 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:53,749 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:53,749 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,749 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,749 INFO  L85        PathProgramCache]: Analyzing trace with hash 1316258471, now seen corresponding path program 1 times
[2025-04-28 21:21:53,749 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,749 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1441578754]
[2025-04-28 21:21:53,750 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,750 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,768 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:53,780 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:53,780 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,780 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,946 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:53,947 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,947 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1441578754]
[2025-04-28 21:21:53,947 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1441578754] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,947 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,947 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:53,947 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2014415527]
[2025-04-28 21:21:53,947 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,947 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:53,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,948 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:53,948 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,948 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,129 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,129 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:54,130 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,130 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:54,131 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,132 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:54,132 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:54,132 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:54,133 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,133 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:54,136 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:54,145 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:54,147 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:54,149 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:54,150 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:54,150 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,150 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:54,150 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,151 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:54,152 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,152 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,152 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:54,152 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:54,152 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,153 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,153 INFO  L85        PathProgramCache]: Analyzing trace with hash -1266746908, now seen corresponding path program 1 times
[2025-04-28 21:21:54,154 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,154 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [736306854]
[2025-04-28 21:21:54,154 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,169 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,192 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,192 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,193 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,336 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:54,337 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,337 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [736306854]
[2025-04-28 21:21:54,338 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [736306854] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,338 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,338 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:54,338 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [768758405]
[2025-04-28 21:21:54,338 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,338 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:54,338 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,342 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:54,342 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,343 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,515 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,515 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:54,516 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,516 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:54,516 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,517 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:54,518 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:54,518 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:54,520 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,521 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,522 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:54,530 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:54,534 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:54,535 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:54,536 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:54,537 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,537 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:54,537 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,538 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:54,539 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,540 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,540 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:54,540 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:54,541 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,541 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,541 INFO  L85        PathProgramCache]: Analyzing trace with hash -2052800928, now seen corresponding path program 1 times
[2025-04-28 21:21:54,542 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,542 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2034304071]
[2025-04-28 21:21:54,542 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,542 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,560 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,570 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,570 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,722 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:54,722 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,722 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2034304071]
[2025-04-28 21:21:54,723 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2034304071] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,723 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,723 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:54,723 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2123949810]
[2025-04-28 21:21:54,723 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,723 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:54,723 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,724 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:54,724 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:54,724 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,904 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,904 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:54,905 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:54,905 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:54,906 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,907 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:54,908 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:54,908 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:54,908 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,910 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:54,910 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:54,919 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:54,921 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:54,923 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:54,926 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:54,926 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,926 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:54,926 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:54,926 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:54,927 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:54,928 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,928 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:54,928 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:54,928 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,932 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,932 INFO  L85        PathProgramCache]: Analyzing trace with hash 1737615295, now seen corresponding path program 1 times
[2025-04-28 21:21:54,933 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,933 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2005048197]
[2025-04-28 21:21:54,933 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,933 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,949 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:54,960 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:54,960 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,960 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,123 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:55,123 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,123 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2005048197]
[2025-04-28 21:21:55,123 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2005048197] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,123 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,123 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,123 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1652649705]
[2025-04-28 21:21:55,124 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,124 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,124 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,124 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,125 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,296 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,296 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:55,297 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,297 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:55,298 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,299 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:55,299 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:55,299 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:55,300 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,300 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,300 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:55,306 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:55,306 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:55,311 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:55,311 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:55,311 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,311 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:55,312 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,312 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:55,313 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:55,313 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,313 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:55,314 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:55,314 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,314 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,314 INFO  L85        PathProgramCache]: Analyzing trace with hash -845390084, now seen corresponding path program 1 times
[2025-04-28 21:21:55,314 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,314 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [207662848]
[2025-04-28 21:21:55,314 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,315 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,326 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:55,335 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:55,335 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,335 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,464 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:55,465 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,465 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [207662848]
[2025-04-28 21:21:55,465 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [207662848] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,465 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,465 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,465 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [82215141]
[2025-04-28 21:21:55,465 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,465 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,465 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,466 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,466 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,466 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,626 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,626 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:55,626 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,627 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:55,627 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,628 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:55,628 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:55,628 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:55,629 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,629 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,630 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:55,639 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:55,639 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:55,640 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:55,641 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:55,641 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,641 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:55,641 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,641 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:55,642 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:55,642 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,642 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:55,643 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:55,643 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,643 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,643 INFO  L85        PathProgramCache]: Analyzing trace with hash 1456112348, now seen corresponding path program 1 times
[2025-04-28 21:21:55,643 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,643 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [940854379]
[2025-04-28 21:21:55,643 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,644 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,655 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:55,664 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:55,664 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,664 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,786 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:55,786 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,786 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [940854379]
[2025-04-28 21:21:55,786 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [940854379] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,786 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,786 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,786 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1061169140]
[2025-04-28 21:21:55,786 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,787 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,787 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,788 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,788 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,788 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,954 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,954 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:55,955 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,956 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:55,956 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,957 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:55,958 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:55,958 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:55,960 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,960 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,961 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:55,967 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:55,967 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:55,968 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:55,969 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:55,969 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,969 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:55,969 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:55,969 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:55,970 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:55,970 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,970 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:55,971 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:55,972 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,972 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,972 INFO  L85        PathProgramCache]: Analyzing trace with hash 951561275, now seen corresponding path program 1 times
[2025-04-28 21:21:55,972 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,973 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [565470114]
[2025-04-28 21:21:55,973 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,973 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,984 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:56,000 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:56,002 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,002 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,121 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:56,122 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [565470114]
[2025-04-28 21:21:56,122 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [565470114] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,122 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,122 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:56,122 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [740073067]
[2025-04-28 21:21:56,122 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,122 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:56,122 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,123 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:56,123 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,123 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:56,281 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,281 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:56,282 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:56,282 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:56,282 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,283 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:56,283 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:56,284 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:56,284 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,284 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,285 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:56,293 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:56,293 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:56,297 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:56,297 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:56,297 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,298 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:56,298 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:56,298 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:56,300 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:56,300 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,300 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:56,300 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:56,300 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,301 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,301 INFO  L85        PathProgramCache]: Analyzing trace with hash -1631444104, now seen corresponding path program 1 times
[2025-04-28 21:21:56,301 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,301 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [221149204]
[2025-04-28 21:21:56,301 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,301 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,314 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:56,328 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:56,328 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,328 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,462 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:56,463 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,463 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [221149204]
[2025-04-28 21:21:56,463 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [221149204] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,463 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,463 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:56,463 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1839825016]
[2025-04-28 21:21:56,463 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,463 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:56,463 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,464 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:56,464 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,464 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:56,626 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,626 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:56,627 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:56,627 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:56,627 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,628 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:56,628 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:56,628 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:56,629 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,629 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,629 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:56,637 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:56,640 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 28 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:56,641 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:56,641 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:56,641 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,642 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:56,642 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:56,642 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:56,643 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:56,643 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,643 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:56,643 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:56,643 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,644 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,645 INFO  L85        PathProgramCache]: Analyzing trace with hash 165507255, now seen corresponding path program 1 times
[2025-04-28 21:21:56,645 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,645 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1960014843]
[2025-04-28 21:21:56,645 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,645 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,655 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:56,663 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:56,663 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,663 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,767 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:56,767 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,767 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1960014843]
[2025-04-28 21:21:56,767 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1960014843] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:56,767 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:56,767 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:56,767 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1253327798]
[2025-04-28 21:21:56,767 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,767 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:56,768 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,768 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:56,768 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:56,768 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:56,944 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,944 INFO  L93              Difference]: Finished difference Result 61 states and 132 transitions.
[2025-04-28 21:21:56,945 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:56,946 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:56,946 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,947 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:56,947 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:56,948 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:56,949 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 3 mSDsluCounter, 426 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 541 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,949 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 541 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,950 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:56,954 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 57.
[2025-04-28 21:21:56,955 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 17 states have (on average 3.3529411764705883) internal successors, (57), 27 states have internal predecessors, (57), 30 states have call successors, (30), 8 states have call predecessors, (30), 9 states have return successors, (36), 22 states have call predecessors, (36), 30 states have call successors, (36)
[2025-04-28 21:21:56,957 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 123 transitions.
[2025-04-28 21:21:56,958 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 123 transitions. Word has length 24
[2025-04-28 21:21:56,958 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,959 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 123 transitions.
[2025-04-28 21:21:56,959 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), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:56,959 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 123 transitions.
[2025-04-28 21:21:56,960 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:56,961 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,961 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,961 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:56,961 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,961 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,962 INFO  L85        PathProgramCache]: Analyzing trace with hash 1243356372, now seen corresponding path program 1 times
[2025-04-28 21:21:56,962 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,962 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1462640193]
[2025-04-28 21:21:56,962 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,962 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,978 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:56,993 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:56,995 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,995 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,345 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:57,345 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,345 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1462640193]
[2025-04-28 21:21:57,345 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1462640193] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,345 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1955992013]
[2025-04-28 21:21:57,346 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,346 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,348 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,354 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:57,356 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,458 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:57,567 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:57,567 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,567 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,576 INFO  L256         TraceCheckSpWp]: Trace formula consists of 591 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,589 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,870 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:57,870 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,389 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:59,390 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1955992013] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,390 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,390 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 20
[2025-04-28 21:21:59,390 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1667301818]
[2025-04-28 21:21:59,390 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,391 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:59,391 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,391 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:59,391 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=334, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:59,392 INFO  L87              Difference]: Start difference. First operand 57 states and 123 transitions. Second operand  has 20 states, 8 states have (on average 3.0) internal successors, (24), 17 states have internal predecessors, (24), 13 states have call successors, (18), 1 states have call predecessors, (18), 8 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:00,134 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,134 INFO  L93              Difference]: Finished difference Result 68 states and 162 transitions.
[2025-04-28 21:22:00,134 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:00,135 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 8 states have (on average 3.0) internal successors, (24), 17 states have internal predecessors, (24), 13 states have call successors, (18), 1 states have call predecessors, (18), 8 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18) Word has length 32
[2025-04-28 21:22:00,135 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,136 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:22:00,136 INFO  L226             Difference]: Without dead ends: 66
[2025-04-28 21:22:00,137 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 80 GetRequests, 52 SyntacticMatches, 3 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 29 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=94, Invalid=608, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:00,137 INFO  L437           NwaCegarLoop]: 109 mSDtfsCounter, 17 mSDsluCounter, 1193 mSDsCounter, 0 mSdLazyCounter, 446 mSolverCounterSat, 38 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 1302 SdHoareTripleChecker+Invalid, 484 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 38 IncrementalHoareTripleChecker+Valid, 446 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,137 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 1302 Invalid, 484 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [38 Valid, 446 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:22:00,138 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-04-28 21:22:00,148 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 60.
[2025-04-28 21:22:00,152 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 60 states, 18 states have (on average 3.2222222222222223) internal successors, (58), 29 states have internal predecessors, (58), 31 states have call successors, (31), 8 states have call predecessors, (31), 10 states have return successors, (45), 24 states have call predecessors, (45), 31 states have call successors, (45)
[2025-04-28 21:22:00,153 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 60 states to 60 states and 134 transitions.
[2025-04-28 21:22:00,153 INFO  L79                 Accepts]: Start accepts. Automaton has 60 states and 134 transitions. Word has length 32
[2025-04-28 21:22:00,154 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,154 INFO  L485      AbstractCegarLoop]: Abstraction has 60 states and 134 transitions.
[2025-04-28 21:22:00,154 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 8 states have (on average 3.0) internal successors, (24), 17 states have internal predecessors, (24), 13 states have call successors, (18), 1 states have call predecessors, (18), 8 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:00,154 INFO  L278                IsEmpty]: Start isEmpty. Operand 60 states and 134 transitions.
[2025-04-28 21:22:00,155 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:00,155 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,155 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,164 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:22:00,356 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:22:00,356 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,356 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,356 INFO  L85        PathProgramCache]: Analyzing trace with hash 1536759379, now seen corresponding path program 1 times
[2025-04-28 21:22:00,357 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,357 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1147978090]
[2025-04-28 21:22:00,357 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,357 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,368 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:00,381 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:00,381 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,382 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,645 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,645 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,645 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1147978090]
[2025-04-28 21:22:00,646 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1147978090] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,646 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1509762892]
[2025-04-28 21:22:00,646 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,646 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,648 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,650 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:22:00,682 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,781 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:00,864 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:00,864 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,864 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,868 INFO  L256         TraceCheckSpWp]: Trace formula consists of 591 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,871 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,111 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:01,112 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:02,617 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:02,617 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1509762892] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:02,617 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:02,617 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:02,617 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [858864684]
[2025-04-28 21:22:02,617 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,618 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:02,618 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,618 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:02,619 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:02,619 INFO  L87              Difference]: Start difference. First operand 60 states and 134 transitions. Second operand  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:03,624 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,625 INFO  L93              Difference]: Finished difference Result 72 states and 178 transitions.
[2025-04-28 21:22:03,625 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:03,626 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18) Word has length 32
[2025-04-28 21:22:03,626 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,627 INFO  L225             Difference]: With dead ends: 72
[2025-04-28 21:22:03,627 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:22:03,628 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 81 GetRequests, 50 SyntacticMatches, 3 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=102, Invalid=768, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:03,628 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 15 mSDsluCounter, 1328 mSDsCounter, 0 mSdLazyCounter, 632 mSolverCounterSat, 60 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 1440 SdHoareTripleChecker+Invalid, 692 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 60 IncrementalHoareTripleChecker+Valid, 632 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,628 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 1440 Invalid, 692 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [60 Valid, 632 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:03,629 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:22:03,640 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 62.
[2025-04-28 21:22:03,643 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 19 states have (on average 3.1052631578947367) internal successors, (59), 31 states have internal predecessors, (59), 31 states have call successors, (31), 8 states have call predecessors, (31), 11 states have return successors, (52), 24 states have call predecessors, (52), 31 states have call successors, (52)
[2025-04-28 21:22:03,645 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 142 transitions.
[2025-04-28 21:22:03,646 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 142 transitions. Word has length 32
[2025-04-28 21:22:03,647 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,647 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 142 transitions.
[2025-04-28 21:22:03,647 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:03,647 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 142 transitions.
[2025-04-28 21:22:03,648 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:03,649 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,650 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,655 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:03,850 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:03,850 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,851 INFO  L85        PathProgramCache]: Analyzing trace with hash 1759687248, now seen corresponding path program 1 times
[2025-04-28 21:22:03,851 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,851 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1940230346]
[2025-04-28 21:22:03,851 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,860 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:03,873 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:03,873 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,133 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:04,134 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,134 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1940230346]
[2025-04-28 21:22:04,134 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1940230346] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,134 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1987907251]
[2025-04-28 21:22:04,134 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,134 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,137 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,138 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:04,142 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,246 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:04,336 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:04,336 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,336 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,340 INFO  L256         TraceCheckSpWp]: Trace formula consists of 591 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,343 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:04,579 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:04,579 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:06,101 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,102 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1987907251] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:06,102 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:06,102 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:06,102 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [984656245]
[2025-04-28 21:22:06,102 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,103 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:06,103 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,103 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:06,104 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:06,104 INFO  L87              Difference]: Start difference. First operand 62 states and 142 transitions. Second operand  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:07,177 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,177 INFO  L93              Difference]: Finished difference Result 74 states and 186 transitions.
[2025-04-28 21:22:07,178 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:07,178 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18) Word has length 32
[2025-04-28 21:22:07,179 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,180 INFO  L225             Difference]: With dead ends: 74
[2025-04-28 21:22:07,180 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:22:07,181 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 81 GetRequests, 50 SyntacticMatches, 3 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=102, Invalid=768, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:07,181 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 10 mSDsluCounter, 1693 mSDsCounter, 0 mSdLazyCounter, 813 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 1805 SdHoareTripleChecker+Invalid, 847 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 813 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,182 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 1805 Invalid, 847 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 813 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:22:07,182 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:22:07,191 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 62.
[2025-04-28 21:22:07,191 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 19 states have (on average 3.1052631578947367) internal successors, (59), 31 states have internal predecessors, (59), 31 states have call successors, (31), 8 states have call predecessors, (31), 11 states have return successors, (52), 24 states have call predecessors, (52), 31 states have call successors, (52)
[2025-04-28 21:22:07,193 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 142 transitions.
[2025-04-28 21:22:07,193 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 142 transitions. Word has length 32
[2025-04-28 21:22:07,193 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,193 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 142 transitions.
[2025-04-28 21:22:07,193 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:07,193 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 142 transitions.
[2025-04-28 21:22:07,195 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:07,195 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,195 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,202 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:07,399 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,400 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,400 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,400 INFO  L85        PathProgramCache]: Analyzing trace with hash 2053090255, now seen corresponding path program 1 times
[2025-04-28 21:22:07,400 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,400 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1545696728]
[2025-04-28 21:22:07,401 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,401 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,408 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:07,420 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:07,420 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,420 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,670 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:07,670 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,670 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1545696728]
[2025-04-28 21:22:07,671 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1545696728] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,671 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1778419339]
[2025-04-28 21:22:07,671 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,671 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,673 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,676 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:07,679 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,794 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:07,881 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:07,881 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,881 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,886 INFO  L256         TraceCheckSpWp]: Trace formula consists of 591 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,888 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,104 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:08,104 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:09,588 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:09,588 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1778419339] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:09,589 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:09,589 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:09,589 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [641862798]
[2025-04-28 21:22:09,589 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:09,589 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:09,589 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:09,590 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:09,590 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:09,590 INFO  L87              Difference]: Start difference. First operand 62 states and 142 transitions. Second operand  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:10,530 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,531 INFO  L93              Difference]: Finished difference Result 74 states and 186 transitions.
[2025-04-28 21:22:10,532 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:10,532 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18) Word has length 32
[2025-04-28 21:22:10,532 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:10,534 INFO  L225             Difference]: With dead ends: 74
[2025-04-28 21:22:10,534 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:22:10,534 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 81 GetRequests, 50 SyntacticMatches, 3 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=102, Invalid=768, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:10,535 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 13 mSDsluCounter, 1437 mSDsCounter, 0 mSdLazyCounter, 661 mSolverCounterSat, 44 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 1549 SdHoareTripleChecker+Invalid, 705 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 44 IncrementalHoareTripleChecker+Valid, 661 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:10,535 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 1549 Invalid, 705 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [44 Valid, 661 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:10,536 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:22:10,543 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 62.
[2025-04-28 21:22:10,543 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 19 states have (on average 3.1052631578947367) internal successors, (59), 31 states have internal predecessors, (59), 31 states have call successors, (31), 8 states have call predecessors, (31), 11 states have return successors, (52), 24 states have call predecessors, (52), 31 states have call successors, (52)
[2025-04-28 21:22:10,544 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 142 transitions.
[2025-04-28 21:22:10,545 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 142 transitions. Word has length 32
[2025-04-28 21:22:10,545 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:10,545 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 142 transitions.
[2025-04-28 21:22:10,545 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:10,545 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 142 transitions.
[2025-04-28 21:22:10,547 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:10,547 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:10,547 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:10,554 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:10,750 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable20
[2025-04-28 21:22:10,751 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:10,751 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:10,751 INFO  L85        PathProgramCache]: Analyzing trace with hash -2018949172, now seen corresponding path program 1 times
[2025-04-28 21:22:10,751 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:10,751 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [914254918]
[2025-04-28 21:22:10,751 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:10,752 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:10,761 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:10,771 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:10,771 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:10,771 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:11,032 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:11,032 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:11,032 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [914254918]
[2025-04-28 21:22:11,032 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [914254918] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:11,032 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1367931485]
[2025-04-28 21:22:11,033 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:11,033 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:11,035 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:11,038 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:11,041 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:22:11,174 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:11,257 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:11,257 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:11,257 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:11,260 INFO  L256         TraceCheckSpWp]: Trace formula consists of 591 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:11,262 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:11,477 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:11,477 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:12,798 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:12,798 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1367931485] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:12,798 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:12,799 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:12,799 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [379927777]
[2025-04-28 21:22:12,799 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,799 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:12,799 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,800 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:12,800 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:12,800 INFO  L87              Difference]: Start difference. First operand 62 states and 142 transitions. Second operand  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:13,752 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:13,753 INFO  L93              Difference]: Finished difference Result 74 states and 186 transitions.
[2025-04-28 21:22:13,753 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:13,753 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18) Word has length 32
[2025-04-28 21:22:13,754 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:13,755 INFO  L225             Difference]: With dead ends: 74
[2025-04-28 21:22:13,755 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:22:13,756 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 81 GetRequests, 50 SyntacticMatches, 3 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=102, Invalid=768, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:13,756 INFO  L437           NwaCegarLoop]: 112 mSDtfsCounter, 12 mSDsluCounter, 1693 mSDsCounter, 0 mSdLazyCounter, 813 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 1805 SdHoareTripleChecker+Invalid, 854 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 813 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:13,757 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 1805 Invalid, 854 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 813 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:22:13,758 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:22:13,766 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 62.
[2025-04-28 21:22:13,766 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 19 states have (on average 3.1052631578947367) internal successors, (59), 31 states have internal predecessors, (59), 31 states have call successors, (31), 8 states have call predecessors, (31), 11 states have return successors, (52), 24 states have call predecessors, (52), 31 states have call successors, (52)
[2025-04-28 21:22:13,767 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 142 transitions.
[2025-04-28 21:22:13,767 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 142 transitions. Word has length 32
[2025-04-28 21:22:13,768 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,768 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 142 transitions.
[2025-04-28 21:22:13,768 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:22:13,768 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 142 transitions.
[2025-04-28 21:22:13,770 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:13,770 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,770 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,779 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:22:13,974 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,975 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,975 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,975 INFO  L85        PathProgramCache]: Analyzing trace with hash -1725546165, now seen corresponding path program 1 times
[2025-04-28 21:22:13,975 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,975 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [946025427]
[2025-04-28 21:22:13,975 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,975 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,987 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:13,997 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:13,997 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,997 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,325 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:14,325 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:14,325 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [946025427]
[2025-04-28 21:22:14,325 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [946025427] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:14,325 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1398890443]
[2025-04-28 21:22:14,325 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:14,326 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:14,328 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:14,330 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:14,333 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:14,469 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:14,549 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:14,549 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:14,549 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:14,552 INFO  L256         TraceCheckSpWp]: Trace formula consists of 591 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:14,554 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:14,739 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:14,739 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:15,951 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:15,951 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1398890443] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:15,951 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:15,951 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:15,952 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1358053216]
[2025-04-28 21:22:15,952 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:15,952 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:15,952 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:15,953 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:15,953 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=50, Invalid=412, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:15,953 INFO  L87              Difference]: Start difference. First operand 62 states and 142 transitions. Second operand  has 22 states, 10 states have (on average 2.8) internal successors, (28), 19 states have internal predecessors, (28), 13 states have call successors, (18), 1 states have call predecessors, (18), 10 states have return successors, (18), 12 states have call predecessors, (18), 13 states have call successors, (18)
