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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,868 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,971 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b92ac016-7974-41cb-a2a3-9eaa65823e1c/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,977 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,977 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:41,010 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:41,012 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:41,012 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:41,013 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:41,014 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:41,015 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:41,015 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:41,015 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:41,015 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:41,016 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:41,016 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:41,016 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:41,016 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:41,016 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,016 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:41,017 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:41,017 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:41,017 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:41,017 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:41,017 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:41,018 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:41,018 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:41,359 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:41,373 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:41,377 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:41,379 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:41,380 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:41,384 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b92ac016-7974-41cb-a2a3-9eaa65823e1c/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-101.smt2
[2025-04-28 21:21:41,386 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:41,390 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:41,678 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b92ac016-7974-41cb-a2a3-9eaa65823e1c/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-101.smt2
[2025-04-28 21:21:41,683 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:41,686 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:41,687 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:41,688 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:41,688 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:41,691 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,735 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41 Unit
[2025-04-28 21:21:41,735 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:41,737 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,738 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:41,738 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:41,752 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,752 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,781 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,781 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,789 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,790 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,796 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,797 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,798 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,823 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,826 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,826 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,826 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,828 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,835 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,851 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,867 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,871 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,887 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,887 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,887 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,887 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:41,887 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:41,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:41,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:41,888 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:41,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:41,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS1__syn given in one single declaration
[2025-04-28 21:21:41,888 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS1__syn
[2025-04-28 21:21:41,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS1__syn
[2025-04-28 21:21:41,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE1__syn given in one single declaration
[2025-04-28 21:21:41,888 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE1__syn
[2025-04-28 21:21:41,888 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE1__syn
[2025-04-28 21:21:41,888 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__syn given in one single declaration
[2025-04-28 21:21:41,889 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__syn
[2025-04-28 21:21:41,889 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__syn
[2025-04-28 21:21:41,889 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:41,889 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:41,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:41,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:41,891 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:41,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:41,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcS1__sem given in one single declaration
[2025-04-28 21:21:41,892 INFO  L130     BoogieDeclarations]: Found specification of procedure funcS1__sem
[2025-04-28 21:21:41,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcS1__sem
[2025-04-28 21:21:41,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE1__sem given in one single declaration
[2025-04-28 21:21:41,892 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE1__sem
[2025-04-28 21:21:41,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE1__sem
[2025-04-28 21:21:41,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__sem given in one single declaration
[2025-04-28 21:21:41,892 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__sem
[2025-04-28 21:21:41,892 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__sem
[2025-04-28 21:21:41,892 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__sem given in one single declaration
[2025-04-28 21:21:41,892 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__sem
[2025-04-28 21:21:41,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__sem
[2025-04-28 21:21:41,893 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,893 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,893 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:42,000 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:42,002 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:42,265 INFO  L?                        ?]: Removed 16 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:42,266 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:42,284 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:42,288 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:42,288 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42 BoogieIcfgContainer
[2025-04-28 21:21:42,288 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:42,291 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:42,291 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:42,295 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:42,296 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/3) ...
[2025-04-28 21:21:42,296 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6c616b33 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,297 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (2/3) ...
[2025-04-28 21:21:42,297 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6c616b33 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,297 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42" (3/3) ...
[2025-04-28 21:21:42,298 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:42,313 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:42,316 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 13 procedures, 52 locations, 66 edges, 13 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:42,366 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:42,385 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;@1ec0847f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:42,385 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:42,390 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 52 states, 25 states have (on average 1.08) internal successors, (27), 27 states have internal predecessors, (27), 13 states have call successors, (13), 12 states have call predecessors, (13), 12 states have return successors, (13), 13 states have call predecessors, (13), 13 states have call successors, (13)
[2025-04-28 21:21:42,399 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:42,400 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,400 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:42,401 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,406 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,407 INFO  L85        PathProgramCache]: Analyzing trace with hash 289001431, now seen corresponding path program 1 times
[2025-04-28 21:21:42,415 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,415 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1273286572]
[2025-04-28 21:21:42,416 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,416 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,456 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:42,485 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:42,486 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,486 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,755 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:42,756 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,756 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1273286572]
[2025-04-28 21:21:42,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1273286572] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,757 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,763 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:42,764 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1631314882]
[2025-04-28 21:21:42,765 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,769 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,770 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,797 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,797 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:42,799 INFO  L87              Difference]: Start difference. First operand  has 52 states, 25 states have (on average 1.08) internal successors, (27), 27 states have internal predecessors, (27), 13 states have call successors, (13), 12 states have call predecessors, (13), 12 states have return successors, (13), 13 states have call predecessors, (13), 13 states have call successors, (13) Second operand  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:42,863 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,863 INFO  L93              Difference]: Finished difference Result 52 states and 53 transitions.
[2025-04-28 21:21:42,866 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:42,868 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 32
[2025-04-28 21:21:42,869 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,876 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:42,877 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:42,879 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:42,885 INFO  L437           NwaCegarLoop]: 50 mSDtfsCounter, 1 mSDsluCounter, 92 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 142 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,886 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 142 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:42,924 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:42,948 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 52.
[2025-04-28 21:21:42,949 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 25 states have (on average 1.04) internal successors, (26), 26 states have internal predecessors, (26), 13 states have call successors, (13), 12 states have call predecessors, (13), 13 states have return successors, (14), 13 states have call predecessors, (14), 13 states have call successors, (14)
[2025-04-28 21:21:42,986 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 53 transitions.
[2025-04-28 21:21:42,987 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 53 transitions. Word has length 32
[2025-04-28 21:21:42,987 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,987 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 53 transitions.
[2025-04-28 21:21:42,988 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.333333333333333) internal successors, (16), 4 states have internal predecessors, (16), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:42,988 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 53 transitions.
[2025-04-28 21:21:42,990 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:42,990 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,990 INFO  L218           NwaCegarLoop]: trace histogram [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, 1]
[2025-04-28 21:21:42,991 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:42,991 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,992 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,992 INFO  L85        PathProgramCache]: Analyzing trace with hash 1587931741, now seen corresponding path program 1 times
[2025-04-28 21:21:42,992 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,992 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [559290472]
[2025-04-28 21:21:42,992 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,992 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:43,126 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:43,126 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,126 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,926 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:43,926 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,927 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [559290472]
[2025-04-28 21:21:43,927 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [559290472] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,927 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2139428666]
[2025-04-28 21:21:43,929 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,930 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,933 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,937 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:43,939 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,081 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:21:44,198 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,198 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,199 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,202 INFO  L256         TraceCheckSpWp]: Trace formula consists of 422 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,213 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,714 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:44,714 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,589 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,589 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2139428666] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,589 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,589 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 16
[2025-04-28 21:21:46,590 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1435421639]
[2025-04-28 21:21:46,591 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,592 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:46,592 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,594 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:46,595 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=194, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:46,596 INFO  L87              Difference]: Start difference. First operand 52 states and 53 transitions. Second operand  has 16 states, 6 states have (on average 6.833333333333333) internal successors, (41), 14 states have internal predecessors, (41), 13 states have call successors, (24), 2 states have call predecessors, (24), 6 states have return successors, (24), 6 states have call predecessors, (24), 13 states have call successors, (24)
[2025-04-28 21:21:46,869 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,869 INFO  L93              Difference]: Finished difference Result 55 states and 57 transitions.
[2025-04-28 21:21:46,870 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:46,870 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 6 states have (on average 6.833333333333333) internal successors, (41), 14 states have internal predecessors, (41), 13 states have call successors, (24), 2 states have call predecessors, (24), 6 states have return successors, (24), 6 states have call predecessors, (24), 13 states have call successors, (24) Word has length 52
[2025-04-28 21:21:46,870 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,871 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:46,871 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:46,872 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 116 GetRequests, 98 SyntacticMatches, 1 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 52 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=67, Invalid=275, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:46,872 INFO  L437           NwaCegarLoop]: 48 mSDtfsCounter, 7 mSDsluCounter, 476 mSDsCounter, 0 mSdLazyCounter, 70 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 524 SdHoareTripleChecker+Invalid, 83 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 70 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,873 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 524 Invalid, 83 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 70 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,874 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:46,880 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 55.
[2025-04-28 21:21:46,881 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 55 states, 26 states have (on average 1.0384615384615385) internal successors, (27), 27 states have internal predecessors, (27), 14 states have call successors, (14), 12 states have call predecessors, (14), 14 states have return successors, (16), 15 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:46,883 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 55 states to 55 states and 57 transitions.
[2025-04-28 21:21:46,884 INFO  L79                 Accepts]: Start accepts. Automaton has 55 states and 57 transitions. Word has length 52
[2025-04-28 21:21:46,884 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,884 INFO  L485      AbstractCegarLoop]: Abstraction has 55 states and 57 transitions.
[2025-04-28 21:21:46,885 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 6 states have (on average 6.833333333333333) internal successors, (41), 14 states have internal predecessors, (41), 13 states have call successors, (24), 2 states have call predecessors, (24), 6 states have return successors, (24), 6 states have call predecessors, (24), 13 states have call successors, (24)
[2025-04-28 21:21:46,885 INFO  L278                IsEmpty]: Start isEmpty. Operand 55 states and 57 transitions.
[2025-04-28 21:21:46,886 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 73
[2025-04-28 21:21:46,888 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,888 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 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]
[2025-04-28 21:21:46,895 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:47,088 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:47,089 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,090 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,090 INFO  L85        PathProgramCache]: Analyzing trace with hash 1342986979, now seen corresponding path program 2 times
[2025-04-28 21:21:47,090 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,090 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [308071796]
[2025-04-28 21:21:47,090 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,090 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,117 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 72 statements into 2 equivalence classes.
[2025-04-28 21:21:47,191 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:47,192 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,192 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,776 INFO  L134       CoverageAnalysis]: Checked inductivity of 26 backedges. 5 proven. 7 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:47,776 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [308071796]
[2025-04-28 21:21:47,776 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [308071796] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [621808357]
[2025-04-28 21:21:47,776 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,777 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,781 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,783 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:47,787 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,922 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 72 statements into 2 equivalence classes.
[2025-04-28 21:21:48,071 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:48,072 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,072 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,080 INFO  L256         TraceCheckSpWp]: Trace formula consists of 662 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,085 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,282 INFO  L134       CoverageAnalysis]: Checked inductivity of 26 backedges. 5 proven. 7 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:48,282 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,008 INFO  L134       CoverageAnalysis]: Checked inductivity of 26 backedges. 5 proven. 7 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:50,009 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [621808357] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,010 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,011 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:50,011 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1051071568]
[2025-04-28 21:21:50,011 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,012 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:50,012 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,013 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:50,014 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:50,014 INFO  L87              Difference]: Start difference. First operand 55 states and 57 transitions. Second operand  has 12 states, 5 states have (on average 9.0) internal successors, (45), 12 states have internal predecessors, (45), 10 states have call successors, (26), 2 states have call predecessors, (26), 5 states have return successors, (26), 4 states have call predecessors, (26), 10 states have call successors, (26)
[2025-04-28 21:21:50,118 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,118 INFO  L93              Difference]: Finished difference Result 29 states and 31 transitions.
[2025-04-28 21:21:50,119 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:50,119 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 5 states have (on average 9.0) internal successors, (45), 12 states have internal predecessors, (45), 10 states have call successors, (26), 2 states have call predecessors, (26), 5 states have return successors, (26), 4 states have call predecessors, (26), 10 states have call successors, (26) Word has length 72
[2025-04-28 21:21:50,119 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,119 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:50,120 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:50,120 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 153 GetRequests, 140 SyntacticMatches, 1 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 14 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=38, Invalid=144, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:50,121 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 2 mSDsluCounter, 124 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 36 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,121 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 146 Invalid, 36 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,122 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:50,122 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:50,123 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:50,123 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:50,123 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 72
[2025-04-28 21:21:50,123 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,123 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:50,123 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 5 states have (on average 9.0) internal successors, (45), 12 states have internal predecessors, (45), 10 states have call successors, (26), 2 states have call predecessors, (26), 5 states have return successors, (26), 4 states have call predecessors, (26), 10 states have call successors, (26)
[2025-04-28 21:21:50,123 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:50,124 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:50,126 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:50,133 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:50,327 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:50,331 INFO  L422         BasicCegarLoop]: Path program histogram: [2, 1]
[2025-04-28 21:21:50,333 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:50,337 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:50 BoogieIcfgContainer
[2025-04-28 21:21:50,337 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:50,338 INFO  L158              Benchmark]: Toolchain (without parser) took 8652.76ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 157.8MB in the beginning and 151.8MB in the end (delta: 6.0MB). Peak memory consumption was 126.5MB. Max. memory is 33.6GB.
[2025-04-28 21:21:50,338 INFO  L158              Benchmark]: SmtParser took 0.78ms. Allocated memory is still 234.9MB. Free memory is still 168.8MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:50,339 INFO  L158              Benchmark]: ChcToBoogie took 48.85ms. Allocated memory is still 234.9MB. Free memory was 157.8MB in the beginning and 156.5MB in the end (delta: 1.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:50,339 INFO  L158              Benchmark]: Boogie Preprocessor took 85.53ms. Allocated memory is still 234.9MB. Free memory was 156.5MB in the beginning and 154.0MB in the end (delta: 2.5MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:50,339 INFO  L158              Benchmark]: RCFGBuilder took 462.34ms. Allocated memory is still 234.9MB. Free memory was 154.0MB in the beginning and 139.1MB in the end (delta: 14.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:50,340 INFO  L158              Benchmark]: TraceAbstraction took 8046.46ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 138.5MB in the beginning and 151.8MB in the end (delta: -13.4MB). Peak memory consumption was 109.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:50,341 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.78ms. Allocated memory is still 234.9MB. Free memory is still 168.8MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 48.85ms. Allocated memory is still 234.9MB. Free memory was 157.8MB in the beginning and 156.5MB in the end (delta: 1.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 85.53ms. Allocated memory is still 234.9MB. Free memory was 156.5MB in the beginning and 154.0MB in the end (delta: 2.5MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 462.34ms. Allocated memory is still 234.9MB. Free memory was 154.0MB in the beginning and 139.1MB in the end (delta: 14.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 8046.46ms. Allocated memory was 234.9MB in the beginning and 352.3MB in the end (delta: 117.4MB). Free memory was 138.5MB in the beginning and 151.8MB in the end (delta: -13.4MB). Peak memory consumption was 109.8MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 13 procedures, 52 locations, 66 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 8.0s, OverallIterations: 3, TraceHistogramMax: 3, PathProgramHistogramMax: 2, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 18 SdHoareTripleChecker+Valid, 0.2s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 10 mSDsluCounter, 812 SdHoareTripleChecker+Invalid, 0.2s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 692 mSDsCounter, 17 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 108 IncrementalHoareTripleChecker+Invalid, 125 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 17 mSolverCounterUnsat, 120 mSDtfsCounter, 108 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 273 GetRequests, 240 SyntacticMatches, 2 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 66 ImplicationChecksByTransitivity, 0.6s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=55occurred in iteration=2, InterpolantAutomatonStates: 22, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 3 MinimizatonAttempts, 0 StatesRemovedByMinimization, 0 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.5s SatisfiabilityAnalysisTime, 6.0s InterpolantComputationTime, 280 NumberOfCodeBlocks, 280 NumberOfCodeBlocksAsserted, 7 NumberOfCheckSat, 397 ConstructedInterpolants, 0 QuantifiedInterpolants, 817 SizeOfPredicates, 21 NumberOfNonLiveVariables, 1084 ConjunctsInSsa, 30 ConjunctsInUnsatCore, 7 InterpolantComputations, 1 PerfectInterpolantSequences, 60/87 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:50,359 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Forceful destruction successful, exit code 0
Received shutdown request...
sat
