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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:18,876 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:18,966 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9122c6a4-4139-4621-9732-008eb2cd1c58/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:18,973 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:18,975 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:19,011 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:19,012 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:19,012 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:19,013 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:19,014 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:19,015 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:19,015 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:19,016 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:19,017 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:19,017 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:19,017 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:19,017 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:19,017 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:19,017 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:19,017 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:19,018 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:19,018 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:19,018 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:19,018 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:19,019 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:19,020 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:19,020 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:19,389 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:19,401 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:19,405 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:19,409 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:19,409 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:19,411 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9122c6a4-4139-4621-9732-008eb2cd1c58/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-058.smt2
[2025-04-28 21:21:19,415 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:19,419 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:19,716 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9122c6a4-4139-4621-9732-008eb2cd1c58/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-058.smt2
[2025-04-28 21:21:19,723 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:19,724 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:19,725 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:19,726 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:19,726 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:19,729 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,782 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19 Unit
[2025-04-28 21:21:19,782 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:19,785 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,785 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:19,785 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:19,804 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,805 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,835 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,835 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,840 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,842 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,844 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,846 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,847 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,865 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,866 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:19,866 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:19,866 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:19,867 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,870 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:19,894 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:19,907 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:19,910 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:19,924 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:19,924 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:19,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:19,924 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:19,924 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:19,924 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:19,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:19,925 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:19,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:19,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__syn given in one single declaration
[2025-04-28 21:21:19,925 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__syn
[2025-04-28 21:21:19,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__syn
[2025-04-28 21:21:19,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:19,925 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:19,925 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:19,925 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:19,926 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:19,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:19,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__sem given in one single declaration
[2025-04-28 21:21:19,926 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__sem
[2025-04-28 21:21:19,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__sem
[2025-04-28 21:21:19,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__sem given in one single declaration
[2025-04-28 21:21:19,926 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__sem
[2025-04-28 21:21:19,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__sem
[2025-04-28 21:21:19,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__sem given in one single declaration
[2025-04-28 21:21:19,926 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__sem
[2025-04-28 21:21:19,926 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__sem
[2025-04-28 21:21:19,926 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__syn given in one single declaration
[2025-04-28 21:21:19,927 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__syn
[2025-04-28 21:21:19,927 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__syn
[2025-04-28 21:21:19,927 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:19,927 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:19,927 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:20,099 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:20,101 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:20,468 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:20,469 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:20,486 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:20,486 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:20,490 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:20 BoogieIcfgContainer
[2025-04-28 21:21:20,491 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:20,493 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:20,493 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:20,502 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:20,505 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/3) ...
[2025-04-28 21:21:20,506 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7caf2f04 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:20, skipping insertion in model container
[2025-04-28 21:21:20,506 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (2/3) ...
[2025-04-28 21:21:20,506 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7caf2f04 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:20, skipping insertion in model container
[2025-04-28 21:21:20,507 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:20" (3/3) ...
[2025-04-28 21:21:20,508 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:20,524 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:20,528 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 11 procedures, 56 locations, 102 edges, 11 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:20,593 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:20,609 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;@2d1e1bc3, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:20,609 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:20,613 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 56 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 27 states have internal predecessors, (33), 23 states have call successors, (23), 10 states have call predecessors, (23), 10 states have return successors, (23), 21 states have call predecessors, (23), 23 states have call successors, (23)
[2025-04-28 21:21:20,626 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:20,627 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,628 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1]
[2025-04-28 21:21:20,628 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,635 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,636 INFO  L85        PathProgramCache]: Analyzing trace with hash -1478006034, now seen corresponding path program 1 times
[2025-04-28 21:21:20,646 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,648 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [566182389]
[2025-04-28 21:21:20,648 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,649 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,718 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:20,877 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:20,878 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,878 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,659 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:21,660 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,660 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [566182389]
[2025-04-28 21:21:21,661 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [566182389] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,661 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,664 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:21,667 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2048708601]
[2025-04-28 21:21:21,670 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,676 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:21,676 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,755 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:21,755 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:21,758 INFO  L87              Difference]: Start difference. First operand  has 56 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 27 states have internal predecessors, (33), 23 states have call successors, (23), 10 states have call predecessors, (23), 10 states have return successors, (23), 21 states have call predecessors, (23), 23 states have call successors, (23) Second operand  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:21,937 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,938 INFO  L93              Difference]: Finished difference Result 59 states and 83 transitions.
[2025-04-28 21:21:21,940 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:21,942 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 4 states have call successors, (9) Word has length 36
[2025-04-28 21:21:21,942 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,957 INFO  L225             Difference]: With dead ends: 59
[2025-04-28 21:21:21,959 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:21,962 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:21,966 INFO  L437           NwaCegarLoop]: 74 mSDtfsCounter, 2 mSDsluCounter, 212 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 286 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,967 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 286 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,983 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:22,021 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:22,024 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 21 states have (on average 1.5238095238095237) internal successors, (32), 26 states have internal predecessors, (32), 23 states have call successors, (23), 10 states have call predecessors, (23), 11 states have return successors, (24), 21 states have call predecessors, (24), 23 states have call successors, (24)
[2025-04-28 21:21:22,033 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 79 transitions.
[2025-04-28 21:21:22,034 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 79 transitions. Word has length 36
[2025-04-28 21:21:22,035 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,036 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 79 transitions.
[2025-04-28 21:21:22,036 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (9), 1 states have call predecessors, (9), 4 states have return successors, (9), 4 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:22,036 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 79 transitions.
[2025-04-28 21:21:22,042 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:22,042 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,042 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,043 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:22,043 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,043 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,044 INFO  L85        PathProgramCache]: Analyzing trace with hash -1064702399, now seen corresponding path program 1 times
[2025-04-28 21:21:22,044 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,044 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1178047025]
[2025-04-28 21:21:22,044 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,046 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,091 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:22,180 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:22,180 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,180 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,824 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:22,825 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1178047025]
[2025-04-28 21:21:22,825 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1178047025] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [325727954]
[2025-04-28 21:21:22,825 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,825 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,831 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,835 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:22,837 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,991 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:23,153 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:23,154 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,154 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,160 INFO  L256         TraceCheckSpWp]: Trace formula consists of 654 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:23,167 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,583 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:23,584 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,025 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:25,025 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [325727954] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,025 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,025 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 19
[2025-04-28 21:21:25,026 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1519111127]
[2025-04-28 21:21:25,027 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,028 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:25,028 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,029 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:25,029 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=300, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:25,029 INFO  L87              Difference]: Start difference. First operand 56 states and 79 transitions. Second operand  has 19 states, 10 states have (on average 3.5) internal successors, (35), 17 states have internal predecessors, (35), 12 states have call successors, (22), 1 states have call predecessors, (22), 10 states have return successors, (22), 8 states have call predecessors, (22), 12 states have call successors, (22)
[2025-04-28 21:21:25,528 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,532 INFO  L93              Difference]: Finished difference Result 67 states and 97 transitions.
[2025-04-28 21:21:25,533 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:25,533 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 10 states have (on average 3.5) internal successors, (35), 17 states have internal predecessors, (35), 12 states have call successors, (22), 1 states have call predecessors, (22), 10 states have return successors, (22), 8 states have call predecessors, (22), 12 states have call successors, (22) Word has length 60
[2025-04-28 21:21:25,533 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,535 INFO  L225             Difference]: With dead ends: 67
[2025-04-28 21:21:25,535 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:25,536 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 136 GetRequests, 109 SyntacticMatches, 3 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 73 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=85, Invalid=565, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:25,539 INFO  L437           NwaCegarLoop]: 74 mSDtfsCounter, 9 mSDsluCounter, 954 mSDsCounter, 0 mSdLazyCounter, 177 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1028 SdHoareTripleChecker+Invalid, 196 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 177 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,539 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1028 Invalid, 196 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 177 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:25,540 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:25,554 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 59.
[2025-04-28 21:21:25,554 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 22 states have (on average 1.5) internal successors, (33), 28 states have internal predecessors, (33), 24 states have call successors, (24), 10 states have call predecessors, (24), 12 states have return successors, (30), 22 states have call predecessors, (30), 24 states have call successors, (30)
[2025-04-28 21:21:25,556 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 87 transitions.
[2025-04-28 21:21:25,559 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 87 transitions. Word has length 60
[2025-04-28 21:21:25,559 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,560 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 87 transitions.
[2025-04-28 21:21:25,560 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 10 states have (on average 3.5) internal successors, (35), 17 states have internal predecessors, (35), 12 states have call successors, (22), 1 states have call predecessors, (22), 10 states have return successors, (22), 8 states have call predecessors, (22), 12 states have call successors, (22)
[2025-04-28 21:21:25,560 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 87 transitions.
[2025-04-28 21:21:25,562 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:25,564 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,565 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:25,574 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:25,765 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,765 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,766 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,766 INFO  L85        PathProgramCache]: Analyzing trace with hash -1481345603, now seen corresponding path program 1 times
[2025-04-28 21:21:25,766 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,766 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1756327466]
[2025-04-28 21:21:25,766 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,767 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,787 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:25,852 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:25,854 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,854 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,418 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:26,418 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,418 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1756327466]
[2025-04-28 21:21:26,418 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1756327466] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:26,419 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [918819219]
[2025-04-28 21:21:26,419 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,419 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,422 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,424 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:26,429 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,563 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 60 statements into 1 equivalence classes.
[2025-04-28 21:21:26,669 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:26,670 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,670 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,679 INFO  L256         TraceCheckSpWp]: Trace formula consists of 654 conjuncts, 28 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:26,687 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,459 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:27,459 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,125 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:31,125 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [918819219] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:31,126 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:31,126 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 16, 16] total 30
[2025-04-28 21:21:31,126 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [588123172]
[2025-04-28 21:21:31,126 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-04-28 21:21:31,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,128 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-04-28 21:21:31,128 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=74, Invalid=796, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:31,129 INFO  L87              Difference]: Start difference. First operand 59 states and 87 transitions. Second operand  has 30 states, 13 states have (on average 3.3076923076923075) internal successors, (43), 23 states have internal predecessors, (43), 21 states have call successors, (31), 1 states have call predecessors, (31), 13 states have return successors, (31), 15 states have call predecessors, (31), 21 states have call successors, (31)
[2025-04-28 21:21:32,546 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,547 INFO  L93              Difference]: Finished difference Result 87 states and 129 transitions.
[2025-04-28 21:21:32,547 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-04-28 21:21:32,547 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 13 states have (on average 3.3076923076923075) internal successors, (43), 23 states have internal predecessors, (43), 21 states have call successors, (31), 1 states have call predecessors, (31), 13 states have return successors, (31), 15 states have call predecessors, (31), 21 states have call successors, (31) Word has length 60
[2025-04-28 21:21:32,548 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,550 INFO  L225             Difference]: With dead ends: 87
[2025-04-28 21:21:32,550 INFO  L226             Difference]: Without dead ends: 74
[2025-04-28 21:21:32,551 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 144 GetRequests, 98 SyntacticMatches, 4 SemanticMatches, 42 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 126 ImplicationChecksByTransitivity, 1.5s TimeCoverageRelationStatistics Valid=190, Invalid=1702, Unknown=0, NotChecked=0, Total=1892
[2025-04-28 21:21:32,552 INFO  L437           NwaCegarLoop]: 68 mSDtfsCounter, 28 mSDsluCounter, 1377 mSDsCounter, 0 mSdLazyCounter, 485 mSolverCounterSat, 62 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 32 SdHoareTripleChecker+Valid, 1445 SdHoareTripleChecker+Invalid, 547 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 62 IncrementalHoareTripleChecker+Valid, 485 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,552 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [32 Valid, 1445 Invalid, 547 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [62 Valid, 485 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:32,553 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-04-28 21:21:32,565 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 68.
[2025-04-28 21:21:32,566 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 25 states have (on average 1.44) internal successors, (36), 32 states have internal predecessors, (36), 27 states have call successors, (27), 10 states have call predecessors, (27), 15 states have return successors, (43), 27 states have call predecessors, (43), 27 states have call successors, (43)
[2025-04-28 21:21:32,568 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 106 transitions.
[2025-04-28 21:21:32,568 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 106 transitions. Word has length 60
[2025-04-28 21:21:32,568 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,569 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 106 transitions.
[2025-04-28 21:21:32,569 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 13 states have (on average 3.3076923076923075) internal successors, (43), 23 states have internal predecessors, (43), 21 states have call successors, (31), 1 states have call predecessors, (31), 13 states have return successors, (31), 15 states have call predecessors, (31), 21 states have call successors, (31)
[2025-04-28 21:21:32,569 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 106 transitions.
[2025-04-28 21:21:32,571 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:32,571 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,572 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:32,578 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:32,775 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,775 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,776 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,776 INFO  L85        PathProgramCache]: Analyzing trace with hash -849795124, now seen corresponding path program 1 times
[2025-04-28 21:21:32,776 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,776 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1859888859]
[2025-04-28 21:21:32,776 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,776 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,794 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:32,832 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:32,836 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,836 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,283 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:33,283 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,284 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1859888859]
[2025-04-28 21:21:33,284 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1859888859] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,284 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [356763512]
[2025-04-28 21:21:33,284 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,284 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,287 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,289 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:33,292 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,433 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:33,561 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:33,561 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,561 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,566 INFO  L256         TraceCheckSpWp]: Trace formula consists of 792 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,573 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,859 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:33,860 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,491 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:35,491 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [356763512] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,491 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,491 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:35,492 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1281196433]
[2025-04-28 21:21:35,492 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,492 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:35,493 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,493 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:35,494 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=453, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:35,494 INFO  L87              Difference]: Start difference. First operand 68 states and 106 transitions. Second operand  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27)
[2025-04-28 21:21:36,070 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,070 INFO  L93              Difference]: Finished difference Result 79 states and 126 transitions.
[2025-04-28 21:21:36,071 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:36,071 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27) Word has length 72
[2025-04-28 21:21:36,072 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,074 INFO  L225             Difference]: With dead ends: 79
[2025-04-28 21:21:36,077 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:21:36,078 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 162 GetRequests, 132 SyntacticMatches, 1 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=106, Invalid=824, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:36,079 INFO  L437           NwaCegarLoop]: 77 mSDtfsCounter, 13 mSDsluCounter, 997 mSDsCounter, 0 mSdLazyCounter, 241 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 1074 SdHoareTripleChecker+Invalid, 268 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 241 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,079 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 1074 Invalid, 268 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 241 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:36,083 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:21:36,103 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 68.
[2025-04-28 21:21:36,105 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 25 states have (on average 1.44) internal successors, (36), 32 states have internal predecessors, (36), 27 states have call successors, (27), 10 states have call predecessors, (27), 15 states have return successors, (43), 27 states have call predecessors, (43), 27 states have call successors, (43)
[2025-04-28 21:21:36,107 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 106 transitions.
[2025-04-28 21:21:36,111 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 106 transitions. Word has length 72
[2025-04-28 21:21:36,111 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,111 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 106 transitions.
[2025-04-28 21:21:36,111 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27)
[2025-04-28 21:21:36,112 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 106 transitions.
[2025-04-28 21:21:36,114 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:36,118 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,118 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:36,126 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:36,319 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,319 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,320 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,320 INFO  L85        PathProgramCache]: Analyzing trace with hash -647971190, now seen corresponding path program 1 times
[2025-04-28 21:21:36,320 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,320 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [646403181]
[2025-04-28 21:21:36,320 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,320 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,341 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:36,379 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:36,379 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,380 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,786 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:36,786 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,787 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [646403181]
[2025-04-28 21:21:36,787 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [646403181] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,787 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1985950756]
[2025-04-28 21:21:36,787 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,787 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,790 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,792 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,797 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,936 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:37,053 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:37,053 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,053 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,058 INFO  L256         TraceCheckSpWp]: Trace formula consists of 792 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,061 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,323 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:37,323 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,827 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:38,828 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1985950756] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,828 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,828 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:38,828 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [953424868]
[2025-04-28 21:21:38,828 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,829 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:38,829 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,830 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:38,830 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=453, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:38,830 INFO  L87              Difference]: Start difference. First operand 68 states and 106 transitions. Second operand  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27)
[2025-04-28 21:21:39,346 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,346 INFO  L93              Difference]: Finished difference Result 81 states and 132 transitions.
[2025-04-28 21:21:39,349 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:39,349 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27) Word has length 72
[2025-04-28 21:21:39,350 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,351 INFO  L225             Difference]: With dead ends: 81
[2025-04-28 21:21:39,355 INFO  L226             Difference]: Without dead ends: 74
[2025-04-28 21:21:39,356 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 162 GetRequests, 132 SyntacticMatches, 1 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=106, Invalid=824, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:39,357 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 16 mSDsluCounter, 1038 mSDsCounter, 0 mSdLazyCounter, 270 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 1113 SdHoareTripleChecker+Invalid, 302 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 270 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,357 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 1113 Invalid, 302 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 270 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:39,358 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-04-28 21:21:39,379 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 68.
[2025-04-28 21:21:39,379 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 25 states have (on average 1.44) internal successors, (36), 31 states have internal predecessors, (36), 27 states have call successors, (27), 10 states have call predecessors, (27), 15 states have return successors, (43), 27 states have call predecessors, (43), 27 states have call successors, (43)
[2025-04-28 21:21:39,382 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 106 transitions.
[2025-04-28 21:21:39,382 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 106 transitions. Word has length 72
[2025-04-28 21:21:39,383 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,383 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 106 transitions.
[2025-04-28 21:21:39,383 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27)
[2025-04-28 21:21:39,384 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 106 transitions.
[2025-04-28 21:21:39,386 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:39,386 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,386 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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:39,393 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:39,590 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:39,591 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,591 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,592 INFO  L85        PathProgramCache]: Analyzing trace with hash -1765876656, now seen corresponding path program 1 times
[2025-04-28 21:21:39,592 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,592 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [275747005]
[2025-04-28 21:21:39,592 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,592 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,618 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:39,655 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:39,656 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,656 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,093 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:40,093 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,093 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [275747005]
[2025-04-28 21:21:40,093 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [275747005] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,093 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [684270249]
[2025-04-28 21:21:40,094 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,094 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,096 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,098 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:40,115 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,264 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:40,379 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:40,379 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,379 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,383 INFO  L256         TraceCheckSpWp]: Trace formula consists of 792 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,386 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,509 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:40,509 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,211 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:42,211 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [684270249] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,211 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,211 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 15
[2025-04-28 21:21:42,211 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1148052615]
[2025-04-28 21:21:42,211 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,212 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:42,212 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,212 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:42,213 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=172, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:42,213 INFO  L87              Difference]: Start difference. First operand 68 states and 106 transitions. Second operand  has 15 states, 6 states have (on average 5.0) internal successors, (30), 13 states have internal predecessors, (30), 11 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 6 states have call predecessors, (22), 11 states have call successors, (22)
[2025-04-28 21:21:42,467 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,467 INFO  L93              Difference]: Finished difference Result 80 states and 130 transitions.
[2025-04-28 21:21:42,468 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:42,468 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 6 states have (on average 5.0) internal successors, (30), 13 states have internal predecessors, (30), 11 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 6 states have call predecessors, (22), 11 states have call successors, (22) Word has length 72
[2025-04-28 21:21:42,469 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,470 INFO  L225             Difference]: With dead ends: 80
[2025-04-28 21:21:42,470 INFO  L226             Difference]: Without dead ends: 73
[2025-04-28 21:21:42,470 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 156 GetRequests, 138 SyntacticMatches, 2 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 23 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=57, Invalid=249, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:42,471 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 7 mSDsluCounter, 719 mSDsCounter, 0 mSdLazyCounter, 176 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 797 SdHoareTripleChecker+Invalid, 182 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 176 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,471 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 797 Invalid, 182 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 176 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:42,472 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 73 states.
[2025-04-28 21:21:42,481 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 73 to 71.
[2025-04-28 21:21:42,481 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 26 states have (on average 1.4230769230769231) internal successors, (37), 33 states have internal predecessors, (37), 28 states have call successors, (28), 10 states have call predecessors, (28), 16 states have return successors, (51), 28 states have call predecessors, (51), 28 states have call successors, (51)
[2025-04-28 21:21:42,482 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 116 transitions.
[2025-04-28 21:21:42,483 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 116 transitions. Word has length 72
[2025-04-28 21:21:42,483 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,483 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 116 transitions.
[2025-04-28 21:21:42,483 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 6 states have (on average 5.0) internal successors, (30), 13 states have internal predecessors, (30), 11 states have call successors, (22), 1 states have call predecessors, (22), 6 states have return successors, (22), 6 states have call predecessors, (22), 11 states have call successors, (22)
[2025-04-28 21:21:42,483 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 116 transitions.
[2025-04-28 21:21:42,485 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:42,485 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,485 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,491 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:42,689 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,689 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,690 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,690 INFO  L85        PathProgramCache]: Analyzing trace with hash -1362228788, now seen corresponding path program 2 times
[2025-04-28 21:21:42,690 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,690 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [260824310]
[2025-04-28 21:21:42,690 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:42,690 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,706 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 72 statements into 2 equivalence classes.
[2025-04-28 21:21:42,732 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:42,732 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:42,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,031 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:43,031 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [260824310]
[2025-04-28 21:21:43,031 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [260824310] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1069540877]
[2025-04-28 21:21:43,032 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:43,032 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,034 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,036 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,040 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,203 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 72 statements into 2 equivalence classes.
[2025-04-28 21:21:43,323 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:43,323 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:43,323 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,328 INFO  L256         TraceCheckSpWp]: Trace formula consists of 792 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,331 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,498 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:43,498 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,520 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:44,520 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1069540877] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,521 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,521 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 19
[2025-04-28 21:21:44,521 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1158477166]
[2025-04-28 21:21:44,521 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,521 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:44,522 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,522 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:44,523 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=300, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:44,523 INFO  L87              Difference]: Start difference. First operand 71 states and 116 transitions. Second operand  has 19 states, 10 states have (on average 3.6) internal successors, (36), 17 states have internal predecessors, (36), 12 states have call successors, (24), 1 states have call predecessors, (24), 10 states have return successors, (24), 8 states have call predecessors, (24), 12 states have call successors, (24)
[2025-04-28 21:21:44,866 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,866 INFO  L93              Difference]: Finished difference Result 80 states and 129 transitions.
[2025-04-28 21:21:44,867 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:44,867 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 10 states have (on average 3.6) internal successors, (36), 17 states have internal predecessors, (36), 12 states have call successors, (24), 1 states have call predecessors, (24), 10 states have return successors, (24), 8 states have call predecessors, (24), 12 states have call successors, (24) Word has length 72
[2025-04-28 21:21:44,867 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,869 INFO  L225             Difference]: With dead ends: 80
[2025-04-28 21:21:44,869 INFO  L226             Difference]: Without dead ends: 73
[2025-04-28 21:21:44,869 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 161 GetRequests, 134 SyntacticMatches, 3 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 73 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=85, Invalid=565, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:44,870 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 9 mSDsluCounter, 1039 mSDsCounter, 0 mSdLazyCounter, 190 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 1120 SdHoareTripleChecker+Invalid, 205 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 190 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,870 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 1120 Invalid, 205 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 190 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:44,871 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 73 states.
[2025-04-28 21:21:44,879 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 73 to 71.
[2025-04-28 21:21:44,879 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 26 states have (on average 1.4230769230769231) internal successors, (37), 33 states have internal predecessors, (37), 28 states have call successors, (28), 10 states have call predecessors, (28), 16 states have return successors, (50), 28 states have call predecessors, (50), 28 states have call successors, (50)
[2025-04-28 21:21:44,880 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 115 transitions.
[2025-04-28 21:21:44,881 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 115 transitions. Word has length 72
[2025-04-28 21:21:44,881 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,881 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 115 transitions.
[2025-04-28 21:21:44,881 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 10 states have (on average 3.6) internal successors, (36), 17 states have internal predecessors, (36), 12 states have call successors, (24), 1 states have call predecessors, (24), 10 states have return successors, (24), 8 states have call predecessors, (24), 12 states have call successors, (24)
[2025-04-28 21:21:44,882 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 115 transitions.
[2025-04-28 21:21:44,883 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:44,883 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,883 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,890 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:45,084 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,084 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,085 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,085 INFO  L85        PathProgramCache]: Analyzing trace with hash -958580920, now seen corresponding path program 1 times
[2025-04-28 21:21:45,085 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,085 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1545529054]
[2025-04-28 21:21:45,085 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,085 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,098 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:45,124 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:45,124 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,124 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,486 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:45,488 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,489 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1545529054]
[2025-04-28 21:21:45,489 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1545529054] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,489 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2082232823]
[2025-04-28 21:21:45,489 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,489 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,492 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,494 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,500 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,711 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:45,812 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:45,812 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,812 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,815 INFO  L256         TraceCheckSpWp]: Trace formula consists of 792 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,817 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,051 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:46,051 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,536 INFO  L134       CoverageAnalysis]: Checked inductivity of 40 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:47,536 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2082232823] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,536 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,536 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:47,536 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1431972648]
[2025-04-28 21:21:47,536 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,537 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:47,537 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,538 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:47,538 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=453, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:47,538 INFO  L87              Difference]: Start difference. First operand 71 states and 115 transitions. Second operand  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27)
[2025-04-28 21:21:48,067 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,067 INFO  L93              Difference]: Finished difference Result 82 states and 135 transitions.
[2025-04-28 21:21:48,067 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:48,068 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27) Word has length 72
[2025-04-28 21:21:48,068 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,069 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:21:48,069 INFO  L226             Difference]: Without dead ends: 75
[2025-04-28 21:21:48,070 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 163 GetRequests, 133 SyntacticMatches, 1 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=106, Invalid=824, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:48,070 INFO  L437           NwaCegarLoop]: 82 mSDtfsCounter, 13 mSDsluCounter, 1440 mSDsCounter, 0 mSdLazyCounter, 322 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 1522 SdHoareTripleChecker+Invalid, 341 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 322 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,071 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 1522 Invalid, 341 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 322 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:48,071 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 75 states.
[2025-04-28 21:21:48,089 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 75 to 73.
[2025-04-28 21:21:48,089 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 73 states, 27 states have (on average 1.4074074074074074) internal successors, (38), 35 states have internal predecessors, (38), 28 states have call successors, (28), 10 states have call predecessors, (28), 17 states have return successors, (55), 28 states have call predecessors, (55), 28 states have call successors, (55)
[2025-04-28 21:21:48,090 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 73 states to 73 states and 121 transitions.
[2025-04-28 21:21:48,090 INFO  L79                 Accepts]: Start accepts. Automaton has 73 states and 121 transitions. Word has length 72
[2025-04-28 21:21:48,091 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,091 INFO  L485      AbstractCegarLoop]: Abstraction has 73 states and 121 transitions.
[2025-04-28 21:21:48,091 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 3.6363636363636362) internal successors, (40), 20 states have internal predecessors, (40), 15 states have call successors, (27), 1 states have call predecessors, (27), 11 states have return successors, (27), 9 states have call predecessors, (27), 15 states have call successors, (27)
[2025-04-28 21:21:48,093 INFO  L278                IsEmpty]: Start isEmpty. Operand 73 states and 121 transitions.
[2025-04-28 21:21:48,095 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:48,095 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,095 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,104 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:48,296 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:48,296 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,296 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,296 INFO  L85        PathProgramCache]: Analyzing trace with hash -756756986, now seen corresponding path program 1 times
[2025-04-28 21:21:48,297 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,297 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [468236290]
[2025-04-28 21:21:48,297 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,297 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,311 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 72 statements into 1 equivalence classes.
[2025-04-28 21:21:48,381 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 72 of 72 statements.
[2025-04-28 21:21:48,381 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,381 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
