./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_value_inheritance_1.sol_0_no_adts_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:29:05,949 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:29:05,999 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f6bc1658-a978-487e-b7c9-3b25e58d6693/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:29:06,003 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:29:06,003 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:29:06,021 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:29:06,022 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:29:06,022 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:29:06,022 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:29:06,022 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:29:06,023 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:29:06,023 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:29:06,023 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:29:06,023 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:29:06,023 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:29:06,023 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:29:06,023 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:06,024 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:29:06,024 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:29:06,025 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:29:06,025 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:29:06,221 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:29:06,228 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:29:06,231 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:29:06,232 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:29:06,232 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:29:06,233 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f6bc1658-a978-487e-b7c9-3b25e58d6693/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_value_inheritance_1.sol_0_no_adts_000.smt2
[2025-05-07 17:29:06,234 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:29:06,236 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:29:06,423 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f6bc1658-a978-487e-b7c9-3b25e58d6693/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/solidity/no_adts/unit_tests/special/msg_value_inheritance_1.sol_0_no_adts_000.smt2
[2025-05-07 17:29:06,426 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:29:06,427 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:29:06,428 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:29:06,428 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:29:06,428 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:29:06,430 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,463 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06 Unit
[2025-05-07 17:29:06,464 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:29:06,464 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:29:06,464 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:29:06,465 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:29:06,476 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,476 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,495 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,495 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,498 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,499 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,501 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,502 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,503 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,512 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:29:06,513 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:29:06,513 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:29:06,513 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:29:06,514 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (1/1) ...
[2025-05-07 17:29:06,516 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:29:06,523 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:29:06,532 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-05-07 17:29:06,534 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:29:06,542 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:29:06,542 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:29:06,542 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:29:06,542 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure error_target_6_0 given in one single declaration
[2025-05-07 17:29:06,542 INFO  L130     BoogieDeclarations]: Found specification of procedure error_target_6_0
[2025-05-07 17:29:06,542 INFO  L138     BoogieDeclarations]: Found implementation of procedure error_target_6_0
[2025-05-07 17:29:06,542 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_constructor_6_C_34_0 given in one single declaration
[2025-05-07 17:29:06,542 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_constructor_6_C_34_0
[2025-05-07 17:29:06,542 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_constructor_6_C_34_0
[2025-05-07 17:29:06,542 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_28_A_15_0 given in one single declaration
[2025-05-07 17:29:06,542 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_28_A_15_0
[2025-05-07 17:29:06,542 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_28_A_15_0
[2025-05-07 17:29:06,542 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_7_constructor_14_34_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_7_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_7_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_27_constructor_14_34_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure block_27_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_27_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_25__13_34_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure block_25__13_34_0
[2025-05-07 17:29:06,543 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_25__13_34_0
[2025-05-07 17:29:06,543 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_24_constructor_14_34_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure block_24_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_24_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_26_return_constructor_14_34_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure block_26_return_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_26_return_constructor_14_34_0
[2025-05-07 17:29:06,543 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_30_A_15_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_30_A_15_0
[2025-05-07 17:29:06,543 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_30_A_15_0
[2025-05-07 17:29:06,543 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_29_A_15_0 given in one single declaration
[2025-05-07 17:29:06,543 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_29_A_15_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_29_A_15_0
[2025-05-07 17:29:06,544 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure implicit_constructor_entry_31_C_34_0 given in one single declaration
[2025-05-07 17:29:06,544 INFO  L130     BoogieDeclarations]: Found specification of procedure implicit_constructor_entry_31_C_34_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure implicit_constructor_entry_31_C_34_0
[2025-05-07 17:29:06,544 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_21_C_34_0 given in one single declaration
[2025-05-07 17:29:06,544 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_21_C_34_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_21_C_34_0
[2025-05-07 17:29:06,544 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure summary_8_constructor_33_34_0 given in one single declaration
[2025-05-07 17:29:06,544 INFO  L130     BoogieDeclarations]: Found specification of procedure summary_8_constructor_33_34_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure summary_8_constructor_33_34_0
[2025-05-07 17:29:06,544 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_19_return_constructor_33_34_0 given in one single declaration
[2025-05-07 17:29:06,544 INFO  L130     BoogieDeclarations]: Found specification of procedure block_19_return_constructor_33_34_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_19_return_constructor_33_34_0
[2025-05-07 17:29:06,544 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_18__32_34_0 given in one single declaration
[2025-05-07 17:29:06,544 INFO  L130     BoogieDeclarations]: Found specification of procedure block_18__32_34_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_18__32_34_0
[2025-05-07 17:29:06,544 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_17_constructor_33_34_0 given in one single declaration
[2025-05-07 17:29:06,544 INFO  L130     BoogieDeclarations]: Found specification of procedure block_17_constructor_33_34_0
[2025-05-07 17:29:06,544 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_17_constructor_33_34_0
[2025-05-07 17:29:06,545 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure block_20_constructor_33_34_0 given in one single declaration
[2025-05-07 17:29:06,545 INFO  L130     BoogieDeclarations]: Found specification of procedure block_20_constructor_33_34_0
[2025-05-07 17:29:06,545 INFO  L138     BoogieDeclarations]: Found implementation of procedure block_20_constructor_33_34_0
[2025-05-07 17:29:06,545 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_after_init_23_C_34_0 given in one single declaration
[2025-05-07 17:29:06,545 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_after_init_23_C_34_0
[2025-05-07 17:29:06,545 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_after_init_23_C_34_0
[2025-05-07 17:29:06,545 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure contract_initializer_entry_22_C_34_0 given in one single declaration
[2025-05-07 17:29:06,545 INFO  L130     BoogieDeclarations]: Found specification of procedure contract_initializer_entry_22_C_34_0
[2025-05-07 17:29:06,545 INFO  L138     BoogieDeclarations]: Found implementation of procedure contract_initializer_entry_22_C_34_0
[2025-05-07 17:29:06,545 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:29:06,545 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:29:06,545 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:29:06,657 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:29:06,659 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:29:06,846 INFO  L?                        ?]: Removed 162 outVars from TransFormulas that were not future-live.
[2025-05-07 17:29:06,846 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:29:06,857 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:29:06,858 INFO  L312             CfgBuilder]: Removed 7 assume(true) statements.
[2025-05-07 17:29:06,858 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:06 BoogieIcfgContainer
[2025-05-07 17:29:06,858 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:29:06,860 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:29:06,860 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:29:06,864 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:29:06,864 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:29:06" (1/3) ...
[2025-05-07 17:29:06,865 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@717e1f42 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:29:06, skipping insertion in model container
[2025-05-07 17:29:06,865 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:29:06" (2/3) ...
[2025-05-07 17:29:06,865 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@717e1f42 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:29:06, skipping insertion in model container
[2025-05-07 17:29:06,865 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:29:06" (3/3) ...
[2025-05-07 17:29:06,866 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:29:06,881 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:29:06,883 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 21 procedures, 88 locations, 135 edges, 21 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:29:06,917 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:29:06,925 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;@35a6730, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:29:06,925 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:29:06,928 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 88 states, 37 states have (on average 1.135135135135135) internal successors, (42), 42 states have internal predecessors, (42), 29 states have call successors, (31), 20 states have call predecessors, (31), 20 states have return successors, (31), 25 states have call predecessors, (31), 29 states have call successors, (31)
[2025-05-07 17:29:06,935 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 43
[2025-05-07 17:29:06,935 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:06,935 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:06,935 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:06,939 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:06,939 INFO  L85        PathProgramCache]: Analyzing trace with hash 1864903949, now seen corresponding path program 1 times
[2025-05-07 17:29:06,944 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:06,944 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2053349308]
[2025-05-07 17:29:06,945 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:06,945 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:06,981 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 42 statements into 1 equivalence classes.
[2025-05-07 17:29:07,001 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 42 of 42 statements.
[2025-05-07 17:29:07,001 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:07,001 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:07,141 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:07,141 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:07,142 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2053349308]
[2025-05-07 17:29:07,142 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2053349308] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:07,142 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:07,144 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:07,145 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [629707365]
[2025-05-07 17:29:07,146 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:07,148 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:07,148 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:07,166 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:07,166 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:07,168 INFO  L87              Difference]: Start difference. First operand  has 88 states, 37 states have (on average 1.135135135135135) internal successors, (42), 42 states have internal predecessors, (42), 29 states have call successors, (31), 20 states have call predecessors, (31), 20 states have return successors, (31), 25 states have call predecessors, (31), 29 states have call successors, (31) Second operand  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:29:07,234 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:07,235 INFO  L93              Difference]: Finished difference Result 90 states and 107 transitions.
[2025-05-07 17:29:07,236 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:29:07,237 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11) Word has length 42
[2025-05-07 17:29:07,238 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:07,248 INFO  L225             Difference]: With dead ends: 90
[2025-05-07 17:29:07,248 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:29:07,250 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-05-07 17:29:07,253 INFO  L437           NwaCegarLoop]: 100 mSDtfsCounter, 1 mSDsluCounter, 184 mSDsCounter, 0 mSdLazyCounter, 14 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 284 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 14 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:07,254 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 284 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 14 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:07,267 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:29:07,296 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 88.
[2025-05-07 17:29:07,298 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 88 states, 37 states have (on average 1.1081081081081081) internal successors, (41), 41 states have internal predecessors, (41), 29 states have call successors, (31), 20 states have call predecessors, (31), 21 states have return successors, (33), 26 states have call predecessors, (33), 29 states have call successors, (33)
[2025-05-07 17:29:07,302 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 88 states to 88 states and 105 transitions.
[2025-05-07 17:29:07,303 INFO  L79                 Accepts]: Start accepts. Automaton has 88 states and 105 transitions. Word has length 42
[2025-05-07 17:29:07,304 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:07,305 INFO  L485      AbstractCegarLoop]: Abstraction has 88 states and 105 transitions.
[2025-05-07 17:29:07,305 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 4 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 4 states have call successors, (11)
[2025-05-07 17:29:07,305 INFO  L278                IsEmpty]: Start isEmpty. Operand 88 states and 105 transitions.
[2025-05-07 17:29:07,307 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 43
[2025-05-07 17:29:07,307 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:07,308 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:07,308 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:29:07,308 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:07,309 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:07,309 INFO  L85        PathProgramCache]: Analyzing trace with hash -1800750417, now seen corresponding path program 1 times
[2025-05-07 17:29:07,309 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:07,309 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [991448704]
[2025-05-07 17:29:07,309 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:07,309 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:07,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 42 statements into 1 equivalence classes.
[2025-05-07 17:29:07,356 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 42 of 42 statements.
[2025-05-07 17:29:07,356 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:07,356 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:07,477 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:07,477 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:07,477 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [991448704]
[2025-05-07 17:29:07,477 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [991448704] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:07,477 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:07,477 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:07,477 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1075074001]
[2025-05-07 17:29:07,477 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:07,478 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:07,478 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:07,479 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:07,479 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:07,479 INFO  L87              Difference]: Start difference. First operand 88 states and 105 transitions. Second operand  has 7 states, 5 states have (on average 4.0) internal successors, (20), 7 states have internal predecessors, (20), 5 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 6 states have call predecessors, (11), 5 states have call successors, (11)
[2025-05-07 17:29:07,579 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:07,579 INFO  L93              Difference]: Finished difference Result 90 states and 107 transitions.
[2025-05-07 17:29:07,580 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:07,580 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 4.0) internal successors, (20), 7 states have internal predecessors, (20), 5 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 6 states have call predecessors, (11), 5 states have call successors, (11) Word has length 42
[2025-05-07 17:29:07,580 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:07,581 INFO  L225             Difference]: With dead ends: 90
[2025-05-07 17:29:07,581 INFO  L226             Difference]: Without dead ends: 90
[2025-05-07 17:29:07,582 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:29:07,582 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 2 mSDsluCounter, 469 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 567 SdHoareTripleChecker+Invalid, 50 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:07,583 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 567 Invalid, 50 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:07,583 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-05-07 17:29:07,590 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 90.
[2025-05-07 17:29:07,591 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 38 states have (on average 1.105263157894737) internal successors, (42), 42 states have internal predecessors, (42), 29 states have call successors, (31), 20 states have call predecessors, (31), 22 states have return successors, (34), 27 states have call predecessors, (34), 29 states have call successors, (34)
[2025-05-07 17:29:07,592 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 107 transitions.
[2025-05-07 17:29:07,592 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 107 transitions. Word has length 42
[2025-05-07 17:29:07,592 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:07,593 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 107 transitions.
[2025-05-07 17:29:07,593 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 4.0) internal successors, (20), 7 states have internal predecessors, (20), 5 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 6 states have call predecessors, (11), 5 states have call successors, (11)
[2025-05-07 17:29:07,593 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 107 transitions.
[2025-05-07 17:29:07,594 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 43
[2025-05-07 17:29:07,594 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:07,594 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:07,595 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:29:07,595 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:07,595 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:07,595 INFO  L85        PathProgramCache]: Analyzing trace with hash -758594159, now seen corresponding path program 1 times
[2025-05-07 17:29:07,595 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:07,595 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1053398354]
[2025-05-07 17:29:07,595 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:07,595 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:07,616 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 42 statements into 1 equivalence classes.
[2025-05-07 17:29:07,635 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 42 of 42 statements.
[2025-05-07 17:29:07,635 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:07,635 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:07,842 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:07,842 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:07,842 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1053398354]
[2025-05-07 17:29:07,842 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1053398354] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:07,842 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:07,842 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-05-07 17:29:07,842 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [67839812]
[2025-05-07 17:29:07,842 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:07,843 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-05-07 17:29:07,843 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:07,843 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-05-07 17:29:07,843 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:29:07,844 INFO  L87              Difference]: Start difference. First operand 90 states and 107 transitions. Second operand  has 11 states, 8 states have (on average 2.5) internal successors, (20), 10 states have internal predecessors, (20), 7 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 7 states have call successors, (11)
[2025-05-07 17:29:07,991 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:07,991 INFO  L93              Difference]: Finished difference Result 94 states and 111 transitions.
[2025-05-07 17:29:07,992 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-05-07 17:29:07,992 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 8 states have (on average 2.5) internal successors, (20), 10 states have internal predecessors, (20), 7 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 7 states have call successors, (11) Word has length 42
[2025-05-07 17:29:07,992 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:07,993 INFO  L225             Difference]: With dead ends: 94
[2025-05-07 17:29:07,993 INFO  L226             Difference]: Without dead ends: 78
[2025-05-07 17:29:07,993 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=24, Invalid=108, Unknown=0, NotChecked=0, Total=132
[2025-05-07 17:29:07,994 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 3 mSDsluCounter, 732 mSDsCounter, 0 mSdLazyCounter, 97 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 827 SdHoareTripleChecker+Invalid, 101 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 97 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:07,994 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 827 Invalid, 101 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 97 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-05-07 17:29:07,994 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 78 states.
[2025-05-07 17:29:07,998 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 78 to 78.
[2025-05-07 17:29:07,998 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 34 states have (on average 1.0588235294117647) internal successors, (36), 36 states have internal predecessors, (36), 24 states have call successors, (25), 19 states have call predecessors, (25), 19 states have return successors, (25), 22 states have call predecessors, (25), 24 states have call successors, (25)
[2025-05-07 17:29:07,999 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 86 transitions.
[2025-05-07 17:29:07,999 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 86 transitions. Word has length 42
[2025-05-07 17:29:07,999 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:07,999 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 86 transitions.
[2025-05-07 17:29:07,999 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 8 states have (on average 2.5) internal successors, (20), 10 states have internal predecessors, (20), 7 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 8 states have call predecessors, (11), 7 states have call successors, (11)
[2025-05-07 17:29:07,999 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 86 transitions.
[2025-05-07 17:29:08,000 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:29:08,000 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:08,000 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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-05-07 17:29:08,001 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-05-07 17:29:08,001 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:08,001 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:08,001 INFO  L85        PathProgramCache]: Analyzing trace with hash -1587045351, now seen corresponding path program 1 times
[2025-05-07 17:29:08,001 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:08,001 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [513470736]
[2025-05-07 17:29:08,001 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:08,001 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:08,027 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:29:08,039 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:29:08,039 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:08,039 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:08,123 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:08,123 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:08,123 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [513470736]
[2025-05-07 17:29:08,123 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [513470736] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:08,123 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:08,123 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:08,123 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [328053568]
[2025-05-07 17:29:08,123 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:08,124 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:08,124 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:08,125 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:08,125 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:08,125 INFO  L87              Difference]: Start difference. First operand 78 states and 86 transitions. Second operand  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:08,185 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:08,185 INFO  L93              Difference]: Finished difference Result 91 states and 106 transitions.
[2025-05-07 17:29:08,185 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:08,186 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18) Word has length 68
[2025-05-07 17:29:08,186 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:08,187 INFO  L225             Difference]: With dead ends: 91
[2025-05-07 17:29:08,187 INFO  L226             Difference]: Without dead ends: 69
[2025-05-07 17:29:08,187 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:08,188 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 2 mSDsluCounter, 414 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 501 SdHoareTripleChecker+Invalid, 52 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:08,188 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 501 Invalid, 52 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:08,189 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 69 states.
[2025-05-07 17:29:08,192 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 69 to 69.
[2025-05-07 17:29:08,192 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 69 states, 32 states have (on average 1.0) internal successors, (32), 32 states have internal predecessors, (32), 18 states have call successors, (18), 18 states have call predecessors, (18), 18 states have return successors, (18), 18 states have call predecessors, (18), 18 states have call successors, (18)
[2025-05-07 17:29:08,193 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 69 states to 69 states and 68 transitions.
[2025-05-07 17:29:08,193 INFO  L79                 Accepts]: Start accepts. Automaton has 69 states and 68 transitions. Word has length 68
[2025-05-07 17:29:08,193 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:08,193 INFO  L485      AbstractCegarLoop]: Abstraction has 69 states and 68 transitions.
[2025-05-07 17:29:08,193 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 5.333333333333333) internal successors, (32), 7 states have internal predecessors, (32), 4 states have call successors, (18), 1 states have call predecessors, (18), 6 states have return successors, (18), 6 states have call predecessors, (18), 4 states have call successors, (18)
[2025-05-07 17:29:08,194 INFO  L278                IsEmpty]: Start isEmpty. Operand 69 states and 68 transitions.
[2025-05-07 17:29:08,195 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 69
[2025-05-07 17:29:08,195 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:08,195 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, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 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-05-07 17:29:08,195 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:29:08,195 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:08,196 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:08,196 INFO  L85        PathProgramCache]: Analyzing trace with hash 444449183, now seen corresponding path program 1 times
[2025-05-07 17:29:08,196 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:08,196 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1219440426]
[2025-05-07 17:29:08,196 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:08,196 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:08,224 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 68 statements into 1 equivalence classes.
[2025-05-07 17:29:08,239 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 68 of 68 statements.
[2025-05-07 17:29:08,239 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:08,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:08,318 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:29:08,318 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:08,318 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1219440426]
[2025-05-07 17:29:08,318 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1219440426] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:08,318 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:08,318 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-05-07 17:29:08,318 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [554995803]
[2025-05-07 17:29:08,318 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:08,319 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-05-07 17:29:08,319 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:08,319 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-05-07 17:29:08,319 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:08,320 INFO  L87              Difference]: Start difference. First operand 69 states and 68 transitions. Second operand  has 7 states, 5 states have (on average 6.4) internal successors, (32), 7 states have internal predecessors, (32), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:29:08,349 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:08,349 INFO  L93              Difference]: Finished difference Result 29 states and 28 transitions.
[2025-05-07 17:29:08,349 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-05-07 17:29:08,349 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 6.4) internal successors, (32), 7 states have internal predecessors, (32), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18) Word has length 68
[2025-05-07 17:29:08,350 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:08,350 INFO  L225             Difference]: With dead ends: 29
[2025-05-07 17:29:08,350 INFO  L226             Difference]: Without dead ends: 0
[2025-05-07 17:29:08,350 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-05-07 17:29:08,351 INFO  L437           NwaCegarLoop]: 26 mSDtfsCounter, 1 mSDsluCounter, 115 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 141 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:08,351 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 141 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:29:08,352 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-05-07 17:29:08,352 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-05-07 17:29:08,352 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-05-07 17:29:08,352 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-05-07 17:29:08,352 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 68
[2025-05-07 17:29:08,352 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:08,352 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-05-07 17:29:08,352 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 6.4) internal successors, (32), 7 states have internal predecessors, (32), 5 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (18), 6 states have call predecessors, (18), 5 states have call successors, (18)
[2025-05-07 17:29:08,353 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-05-07 17:29:08,353 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-05-07 17:29:08,355 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-05-07 17:29:08,356 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:29:08,359 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1]
[2025-05-07 17:29:08,361 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-05-07 17:29:08,364 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 07.05 05:29:08 BoogieIcfgContainer
[2025-05-07 17:29:08,364 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-05-07 17:29:08,365 INFO  L158              Benchmark]: Toolchain (without parser) took 1937.62ms. Allocated memory is still 234.9MB. Free memory was 154.3MB in the beginning and 102.2MB in the end (delta: 52.1MB). Peak memory consumption was 59.4MB. Max. memory is 33.6GB.
[2025-05-07 17:29:08,365 INFO  L158              Benchmark]: SmtParser took 0.25ms. Allocated memory is still 234.9MB. Free memory is still 173.0MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:08,365 INFO  L158              Benchmark]: ChcToBoogie took 36.15ms. Allocated memory is still 234.9MB. Free memory was 154.3MB in the beginning and 151.4MB in the end (delta: 2.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-05-07 17:29:08,365 INFO  L158              Benchmark]: Boogie Preprocessor took 48.21ms. Allocated memory is still 234.9MB. Free memory was 151.4MB in the beginning and 147.1MB in the end (delta: 4.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-05-07 17:29:08,366 INFO  L158              Benchmark]: RCFGBuilder took 345.09ms. Allocated memory is still 234.9MB. Free memory was 147.0MB in the beginning and 190.2MB in the end (delta: -43.2MB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
[2025-05-07 17:29:08,366 INFO  L158              Benchmark]: TraceAbstraction took 1503.78ms. Allocated memory is still 234.9MB. Free memory was 189.6MB in the beginning and 102.2MB in the end (delta: 87.5MB). Peak memory consumption was 84.2MB. Max. memory is 33.6GB.
[2025-05-07 17:29:08,367 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.25ms. Allocated memory is still 234.9MB. Free memory is still 173.0MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 36.15ms. Allocated memory is still 234.9MB. Free memory was 154.3MB in the beginning and 151.4MB in the end (delta: 2.9MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * Boogie Preprocessor took 48.21ms. Allocated memory is still 234.9MB. Free memory was 151.4MB in the beginning and 147.1MB in the end (delta: 4.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 345.09ms. Allocated memory is still 234.9MB. Free memory was 147.0MB in the beginning and 190.2MB in the end (delta: -43.2MB). Peak memory consumption was 42.3MB. Max. memory is 33.6GB.
 * TraceAbstraction took 1503.78ms. Allocated memory is still 234.9MB. Free memory was 189.6MB in the beginning and 102.2MB in the end (delta: 87.5MB). Peak memory consumption was 84.2MB. 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 21 procedures, 88 locations, 135 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 1.5s, OverallIterations: 5, TraceHistogramMax: 1, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 0.5s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 29 SdHoareTripleChecker+Valid, 0.3s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 9 mSDsluCounter, 2320 SdHoareTripleChecker+Invalid, 0.3s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 1914 mSDsCounter, 11 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 222 IncrementalHoareTripleChecker+Invalid, 233 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 11 mSolverCounterUnsat, 406 mSDtfsCounter, 222 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 39 GetRequests, 10 SyntacticMatches, 0 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=90occurred in iteration=2, InterpolantAutomatonStates: 36, 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, 5 MinimizatonAttempts, 2 StatesRemovedByMinimization, 1 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.1s SatisfiabilityAnalysisTime, 0.6s InterpolantComputationTime, 262 NumberOfCodeBlocks, 262 NumberOfCodeBlocksAsserted, 5 NumberOfCheckSat, 257 ConstructedInterpolants, 0 QuantifiedInterpolants, 388 SizeOfPredicates, 0 NumberOfNonLiveVariables, 0 ConjunctsInSsa, 0 ConjunctsInUnsatCore, 5 InterpolantComputations, 5 PerfectInterpolantSequences, 0/0 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-05-07 17:29:08,380 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
