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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:35,749 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:35,848 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2e9077f5-9192-44bb-9716-d66bc208e235/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:35,854 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:35,858 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:35,891 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:35,892 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:35,892 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:35,894 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:35,894 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:35,894 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:35,895 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:35,895 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:35,895 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:35,895 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:35,897 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,897 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:35,897 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:35,898 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:35,898 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:36,179 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:36,187 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:36,189 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:36,190 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:36,190 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:36,191 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2e9077f5-9192-44bb-9716-d66bc208e235/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-102.smt2
[2025-04-28 21:21:36,193 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:36,196 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:36,795 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2e9077f5-9192-44bb-9716-d66bc208e235/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-102.smt2
[2025-04-28 21:21:36,799 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:36,804 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:36,805 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:36,805 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:36,805 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:36,810 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,884 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36 Unit
[2025-04-28 21:21:36,885 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:36,885 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:36,886 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:36,886 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:36,900 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,901 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,930 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,930 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,939 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,941 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,943 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,947 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,949 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,988 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:36,989 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:36,989 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:36,989 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:36,990 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (1/1) ...
[2025-04-28 21:21:36,994 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:37,010 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,024 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:37,029 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:37,041 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:37,041 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:37,041 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:37,041 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:37,041 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:37,041 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:37,042 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:37,042 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:37,042 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:37,042 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__syn given in one single declaration
[2025-04-28 21:21:37,042 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__syn
[2025-04-28 21:21:37,043 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__syn
[2025-04-28 21:21:37,043 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:37,043 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:37,043 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:37,043 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__sem given in one single declaration
[2025-04-28 21:21:37,043 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__sem
[2025-04-28 21:21:37,043 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__sem
[2025-04-28 21:21:37,044 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__sem given in one single declaration
[2025-04-28 21:21:37,044 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__sem
[2025-04-28 21:21:37,044 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__sem
[2025-04-28 21:21:37,044 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcA__sem given in one single declaration
[2025-04-28 21:21:37,044 INFO  L130     BoogieDeclarations]: Found specification of procedure funcA__sem
[2025-04-28 21:21:37,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcA__sem
[2025-04-28 21:21:37,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__sem given in one single declaration
[2025-04-28 21:21:37,045 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__sem
[2025-04-28 21:21:37,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__sem
[2025-04-28 21:21:37,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS__syn given in one single declaration
[2025-04-28 21:21:37,045 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS__syn
[2025-04-28 21:21:37,045 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS__syn
[2025-04-28 21:21:37,045 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcA__syn given in one single declaration
[2025-04-28 21:21:37,045 INFO  L130     BoogieDeclarations]: Found specification of procedure funcA__syn
[2025-04-28 21:21:37,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcA__syn
[2025-04-28 21:21:37,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:37,046 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:37,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:37,046 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:37,046 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:37,046 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:37,268 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:37,270 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:37,925 INFO  L?                        ?]: Removed 156 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:37,925 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:37,941 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:37,945 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:37,945 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:37 BoogieIcfgContainer
[2025-04-28 21:21:37,945 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:37,950 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:37,950 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:37,955 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:37,956 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:36" (1/3) ...
[2025-04-28 21:21:37,957 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@278391 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:37, skipping insertion in model container
[2025-04-28 21:21:37,957 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:36" (2/3) ...
[2025-04-28 21:21:37,957 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@278391 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:37, skipping insertion in model container
[2025-04-28 21:21:37,957 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:37" (3/3) ...
[2025-04-28 21:21:37,959 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:37,977 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:37,979 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 13 procedures, 76 locations, 160 edges, 13 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:38,037 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:38,052 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;@4ec56460, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:38,052 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:38,058 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 76 states, 25 states have (on average 1.96) internal successors, (49), 41 states have internal predecessors, (49), 37 states have call successors, (37), 12 states have call predecessors, (37), 12 states have return successors, (37), 23 states have call predecessors, (37), 37 states have call successors, (37)
[2025-04-28 21:21:38,075 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:38,075 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,076 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,076 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,083 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,084 INFO  L85        PathProgramCache]: Analyzing trace with hash 1567875308, now seen corresponding path program 1 times
[2025-04-28 21:21:38,093 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,093 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [956813213]
[2025-04-28 21:21:38,093 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,094 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,166 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:38,295 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:38,295 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,295 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,048 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:40,048 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,048 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [956813213]
[2025-04-28 21:21:40,049 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [956813213] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,049 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,053 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:40,055 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [115406188]
[2025-04-28 21:21:40,055 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,061 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:40,062 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,109 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:40,110 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:40,113 INFO  L87              Difference]: Start difference. First operand  has 76 states, 25 states have (on average 1.96) internal successors, (49), 41 states have internal predecessors, (49), 37 states have call successors, (37), 12 states have call predecessors, (37), 12 states have return successors, (37), 23 states have call predecessors, (37), 37 states have call successors, (37) Second operand  has 10 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 6 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:40,574 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,575 INFO  L93              Difference]: Finished difference Result 85 states and 138 transitions.
[2025-04-28 21:21:40,576 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:40,577 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 6 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 6 states have call successors, (8) Word has length 32
[2025-04-28 21:21:40,578 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,586 INFO  L225             Difference]: With dead ends: 85
[2025-04-28 21:21:40,586 INFO  L226             Difference]: Without dead ends: 82
[2025-04-28 21:21:40,588 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=31, Invalid=101, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:40,591 INFO  L437           NwaCegarLoop]: 115 mSDtfsCounter, 4 mSDsluCounter, 894 mSDsCounter, 0 mSdLazyCounter, 85 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 1009 SdHoareTripleChecker+Invalid, 88 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 85 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,592 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 1009 Invalid, 88 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 85 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:40,606 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-04-28 21:21:40,644 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 79.
[2025-04-28 21:21:40,648 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 26 states have (on average 1.8846153846153846) internal successors, (49), 41 states have internal predecessors, (49), 38 states have call successors, (38), 12 states have call predecessors, (38), 14 states have return successors, (43), 25 states have call predecessors, (43), 38 states have call successors, (43)
[2025-04-28 21:21:40,655 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 130 transitions.
[2025-04-28 21:21:40,659 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 130 transitions. Word has length 32
[2025-04-28 21:21:40,661 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,661 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 130 transitions.
[2025-04-28 21:21:40,661 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 6 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 6 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:40,661 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 130 transitions.
[2025-04-28 21:21:40,667 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:40,667 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,667 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:40,667 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:40,667 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,668 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,668 INFO  L85        PathProgramCache]: Analyzing trace with hash -1200202102, now seen corresponding path program 1 times
[2025-04-28 21:21:40,668 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,668 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1688214340]
[2025-04-28 21:21:40,671 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,671 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,716 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:40,743 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:40,743 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,743 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,078 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:42,078 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,078 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1688214340]
[2025-04-28 21:21:42,078 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1688214340] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,078 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,078 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:42,078 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2099945416]
[2025-04-28 21:21:42,078 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,079 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:42,079 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,080 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:42,080 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:42,082 INFO  L87              Difference]: Start difference. First operand 79 states and 130 transitions. Second operand  has 10 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 6 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:42,578 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,578 INFO  L93              Difference]: Finished difference Result 88 states and 144 transitions.
[2025-04-28 21:21:42,579 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:42,579 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 6 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 6 states have call successors, (9) Word has length 36
[2025-04-28 21:21:42,580 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,581 INFO  L225             Difference]: With dead ends: 88
[2025-04-28 21:21:42,582 INFO  L226             Difference]: Without dead ends: 85
[2025-04-28 21:21:42,582 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=36, Invalid=120, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:42,583 INFO  L437           NwaCegarLoop]: 114 mSDtfsCounter, 6 mSDsluCounter, 882 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 996 SdHoareTripleChecker+Invalid, 85 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,583 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 996 Invalid, 85 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:42,584 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 85 states.
[2025-04-28 21:21:42,596 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 85 to 79.
[2025-04-28 21:21:42,601 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 26 states have (on average 1.8846153846153846) internal successors, (49), 41 states have internal predecessors, (49), 38 states have call successors, (38), 12 states have call predecessors, (38), 14 states have return successors, (43), 25 states have call predecessors, (43), 38 states have call successors, (43)
[2025-04-28 21:21:42,602 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 130 transitions.
[2025-04-28 21:21:42,603 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 130 transitions. Word has length 36
[2025-04-28 21:21:42,603 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,603 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 130 transitions.
[2025-04-28 21:21:42,603 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 6 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:42,603 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 130 transitions.
[2025-04-28 21:21:42,610 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:42,610 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,610 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:42,611 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:42,611 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,611 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,611 INFO  L85        PathProgramCache]: Analyzing trace with hash 9302449, now seen corresponding path program 1 times
[2025-04-28 21:21:42,611 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,611 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1679307561]
[2025-04-28 21:21:42,612 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,612 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,669 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 48 statements into 1 equivalence classes.
[2025-04-28 21:21:42,687 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:42,687 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,687 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,984 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:43,984 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,985 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1679307561]
[2025-04-28 21:21:43,985 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1679307561] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,985 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,985 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:43,985 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1877167701]
[2025-04-28 21:21:43,985 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,985 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:43,985 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,986 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:43,986 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=89, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:43,986 INFO  L87              Difference]: Start difference. First operand 79 states and 130 transitions. Second operand  has 11 states, 6 states have (on average 3.0) internal successors, (18), 8 states have internal predecessors, (18), 7 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 7 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:44,438 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,438 INFO  L93              Difference]: Finished difference Result 94 states and 160 transitions.
[2025-04-28 21:21:44,438 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:44,438 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 6 states have (on average 3.0) internal successors, (18), 8 states have internal predecessors, (18), 7 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 7 states have call predecessors, (11), 7 states have call successors, (11) Word has length 48
[2025-04-28 21:21:44,439 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,442 INFO  L225             Difference]: With dead ends: 94
[2025-04-28 21:21:44,443 INFO  L226             Difference]: Without dead ends: 91
[2025-04-28 21:21:44,443 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 16 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:44,444 INFO  L437           NwaCegarLoop]: 120 mSDtfsCounter, 6 mSDsluCounter, 909 mSDsCounter, 0 mSdLazyCounter, 132 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 1029 SdHoareTripleChecker+Invalid, 135 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 132 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,444 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 1029 Invalid, 135 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 132 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:44,445 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-04-28 21:21:44,467 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 82.
[2025-04-28 21:21:44,470 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 27 states have (on average 1.8518518518518519) internal successors, (50), 42 states have internal predecessors, (50), 39 states have call successors, (39), 12 states have call predecessors, (39), 15 states have return successors, (49), 27 states have call predecessors, (49), 39 states have call successors, (49)
[2025-04-28 21:21:44,473 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 138 transitions.
[2025-04-28 21:21:44,473 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 138 transitions. Word has length 48
[2025-04-28 21:21:44,474 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,474 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 138 transitions.
[2025-04-28 21:21:44,474 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 6 states have (on average 3.0) internal successors, (18), 8 states have internal predecessors, (18), 7 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 7 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:44,474 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 138 transitions.
[2025-04-28 21:21:44,480 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:44,480 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,480 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:44,481 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:44,481 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,481 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,481 INFO  L85        PathProgramCache]: Analyzing trace with hash 1685822260, now seen corresponding path program 1 times
[2025-04-28 21:21:44,481 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,481 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [189862753]
[2025-04-28 21:21:44,482 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,482 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,523 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:44,545 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:44,547 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,548 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,165 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:46,166 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,166 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [189862753]
[2025-04-28 21:21:46,166 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [189862753] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,166 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1126932451]
[2025-04-28 21:21:46,166 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,166 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,169 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,173 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:46,176 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,389 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:46,526 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:46,527 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,527 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,532 INFO  L256         TraceCheckSpWp]: Trace formula consists of 627 conjuncts, 45 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,548 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,654 INFO  L189   IndexEqualityManager]: detected not equals via solver
[2025-04-28 21:21:46,660 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 2 stores, 0 select indices, 0 select index equivalence classes, 4 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 40 treesize of output 46
[2025-04-28 21:21:48,035 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:48,036 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,371 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 7 treesize of output 5
[2025-04-28 21:21:56,068 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:56,068 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1126932451] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,068 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,069 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 26
[2025-04-28 21:21:56,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [128498554]
[2025-04-28 21:21:56,069 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,069 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:56,070 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,070 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:56,071 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=79, Invalid=571, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:56,071 INFO  L87              Difference]: Start difference. First operand 82 states and 138 transitions. Second operand  has 26 states, 11 states have (on average 2.727272727272727) internal successors, (30), 17 states have internal predecessors, (30), 20 states have call successors, (25), 1 states have call predecessors, (25), 11 states have return successors, (27), 17 states have call predecessors, (27), 20 states have call successors, (27)
[2025-04-28 21:21:57,279 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,279 INFO  L93              Difference]: Finished difference Result 102 states and 182 transitions.
[2025-04-28 21:21:57,279 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:57,279 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 11 states have (on average 2.727272727272727) internal successors, (30), 17 states have internal predecessors, (30), 20 states have call successors, (25), 1 states have call predecessors, (25), 11 states have return successors, (27), 17 states have call predecessors, (27), 20 states have call successors, (27) Word has length 52
[2025-04-28 21:21:57,280 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,281 INFO  L225             Difference]: With dead ends: 102
[2025-04-28 21:21:57,281 INFO  L226             Difference]: Without dead ends: 99
[2025-04-28 21:21:57,282 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 121 GetRequests, 86 SyntacticMatches, 6 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 241 ImplicationChecksByTransitivity, 1.3s TimeCoverageRelationStatistics Valid=125, Invalid=805, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:57,283 INFO  L437           NwaCegarLoop]: 125 mSDtfsCounter, 12 mSDsluCounter, 1741 mSDsCounter, 0 mSdLazyCounter, 410 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 1866 SdHoareTripleChecker+Invalid, 435 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 410 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,283 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 1866 Invalid, 435 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 410 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:57,284 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 99 states.
[2025-04-28 21:21:57,297 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 99 to 83.
[2025-04-28 21:21:57,297 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 83 states, 27 states have (on average 1.8518518518518519) internal successors, (50), 42 states have internal predecessors, (50), 40 states have call successors, (40), 12 states have call predecessors, (40), 15 states have return successors, (52), 28 states have call predecessors, (52), 40 states have call successors, (52)
[2025-04-28 21:21:57,299 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 83 states to 83 states and 142 transitions.
[2025-04-28 21:21:57,299 INFO  L79                 Accepts]: Start accepts. Automaton has 83 states and 142 transitions. Word has length 52
[2025-04-28 21:21:57,299 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,299 INFO  L485      AbstractCegarLoop]: Abstraction has 83 states and 142 transitions.
[2025-04-28 21:21:57,300 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 11 states have (on average 2.727272727272727) internal successors, (30), 17 states have internal predecessors, (30), 20 states have call successors, (25), 1 states have call predecessors, (25), 11 states have return successors, (27), 17 states have call predecessors, (27), 20 states have call successors, (27)
[2025-04-28 21:21:57,300 INFO  L278                IsEmpty]: Start isEmpty. Operand 83 states and 142 transitions.
[2025-04-28 21:21:57,301 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:57,301 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,302 INFO  L218           NwaCegarLoop]: trace histogram [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]
[2025-04-28 21:21:57,310 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:57,506 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,506 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,506 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,506 INFO  L85        PathProgramCache]: Analyzing trace with hash 1810127567, now seen corresponding path program 1 times
[2025-04-28 21:21:57,506 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,507 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1030343427]
[2025-04-28 21:21:57,507 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,507 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,547 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:57,568 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:57,568 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,568 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,061 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:59,061 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,061 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1030343427]
[2025-04-28 21:21:59,061 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1030343427] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:59,062 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1300849334]
[2025-04-28 21:21:59,062 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,062 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,064 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:59,067 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:59,070 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:59,267 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:59,357 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:59,357 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,357 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,361 INFO  L256         TraceCheckSpWp]: Trace formula consists of 627 conjuncts, 45 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:59,365 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:59,385 INFO  L189   IndexEqualityManager]: detected not equals via solver
[2025-04-28 21:21:59,389 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 2 stores, 0 select indices, 0 select index equivalence classes, 4 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 40 treesize of output 46
[2025-04-28 21:21:59,412 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 3 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 24 treesize of output 3
[2025-04-28 21:22:00,626 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:00,626 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:06,711 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 7 treesize of output 5
[2025-04-28 21:22:07,345 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:07,345 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1300849334] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:07,345 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:07,345 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 27
[2025-04-28 21:22:07,345 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1578916155]
[2025-04-28 21:22:07,345 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,346 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:22:07,346 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,347 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:22:07,347 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=67, Invalid=635, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:07,347 INFO  L87              Difference]: Start difference. First operand 83 states and 142 transitions. Second operand  has 27 states, 12 states have (on average 2.6666666666666665) internal successors, (32), 18 states have internal predecessors, (32), 20 states have call successors, (25), 1 states have call predecessors, (25), 12 states have return successors, (27), 17 states have call predecessors, (27), 20 states have call successors, (27)
