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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:36,625 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:36,731 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33bf000e-9b86-480b-ad63-116729bf6081/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:36,737 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:36,737 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:36,764 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:36,765 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:36,765 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:36,765 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:36,766 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:36,766 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:36,766 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:36,766 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:36,767 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:36,767 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:36,767 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:36,767 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:36,767 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:36,768 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:36,768 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:36,768 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:36,768 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:36,768 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:36,768 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:36,769 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:36,770 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:36,770 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:37,109 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:37,121 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:37,124 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:37,127 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:37,127 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:37,129 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33bf000e-9b86-480b-ad63-116729bf6081/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-147.smt2
[2025-04-28 21:21:37,131 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:37,135 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:37,430 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33bf000e-9b86-480b-ad63-116729bf6081/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-147.smt2
[2025-04-28 21:21:37,434 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:37,436 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:37,438 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:37,439 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:37,439 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:37,445 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,495 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37 Unit
[2025-04-28 21:21:37,496 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:37,497 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:37,498 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:37,498 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:37,515 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,515 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,551 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,551 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,558 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,559 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,566 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,567 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,568 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,593 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:37,594 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:37,594 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:37,594 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:37,595 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (1/1) ...
[2025-04-28 21:21:37,599 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:37,613 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,630 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,634 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:37,647 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:37,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:37,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure realizable given in one single declaration
[2025-04-28 21:21:37,648 INFO  L130     BoogieDeclarations]: Found specification of procedure realizable
[2025-04-28 21:21:37,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure realizable
[2025-04-28 21:21:37,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__sem given in one single declaration
[2025-04-28 21:21:37,648 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__sem
[2025-04-28 21:21:37,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__sem
[2025-04-28 21:21:37,649 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__sem given in one single declaration
[2025-04-28 21:21:37,649 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__sem
[2025-04-28 21:21:37,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__sem
[2025-04-28 21:21:37,649 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__sem given in one single declaration
[2025-04-28 21:21:37,649 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__sem
[2025-04-28 21:21:37,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__sem
[2025-04-28 21:21:37,649 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcStart__syn given in one single declaration
[2025-04-28 21:21:37,649 INFO  L130     BoogieDeclarations]: Found specification of procedure funcStart__syn
[2025-04-28 21:21:37,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcStart__syn
[2025-04-28 21:21:37,650 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcE__syn given in one single declaration
[2025-04-28 21:21:37,650 INFO  L130     BoogieDeclarations]: Found specification of procedure funcE__syn
[2025-04-28 21:21:37,650 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcE__syn
[2025-04-28 21:21:37,650 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure funcB__syn given in one single declaration
[2025-04-28 21:21:37,650 INFO  L130     BoogieDeclarations]: Found specification of procedure funcB__syn
[2025-04-28 21:21:37,650 INFO  L138     BoogieDeclarations]: Found implementation of procedure funcB__syn
[2025-04-28 21:21:37,650 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:37,650 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:37,651 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:37,752 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:37,754 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:38,060 INFO  L?                        ?]: Removed 18 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:38,060 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:38,078 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:38,080 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:38,081 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:38 BoogieIcfgContainer
[2025-04-28 21:21:38,081 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:38,085 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:38,085 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:38,091 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:38,092 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:37" (1/3) ...
[2025-04-28 21:21:38,093 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@45c1bc11 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:38, skipping insertion in model container
[2025-04-28 21:21:38,093 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:37" (2/3) ...
[2025-04-28 21:21:38,093 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@45c1bc11 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:38, skipping insertion in model container
[2025-04-28 21:21:38,093 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:38" (3/3) ...
[2025-04-28 21:21:38,095 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:38,116 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:38,121 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 9 procedures, 42 locations, 68 edges, 9 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:38,171 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:38,190 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;@59891a10, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:38,191 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:38,195 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 42 states, 17 states have (on average 1.3529411764705883) internal successors, (23), 23 states have internal predecessors, (23), 15 states have call successors, (15), 8 states have call predecessors, (15), 8 states have return successors, (15), 11 states have call predecessors, (15), 15 states have call successors, (15)
[2025-04-28 21:21:38,206 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:38,206 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,207 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]
[2025-04-28 21:21:38,207 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,214 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,214 INFO  L85        PathProgramCache]: Analyzing trace with hash 1076346975, now seen corresponding path program 1 times
[2025-04-28 21:21:38,223 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,224 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1340293700]
[2025-04-28 21:21:38,224 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,225 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,261 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:38,310 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:38,313 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,314 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,535 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:38,536 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,536 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1340293700]
[2025-04-28 21:21:38,537 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1340293700] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,537 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,541 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:38,543 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1308925485]
[2025-04-28 21:21:38,544 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,550 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:38,554 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,601 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:38,602 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:38,604 INFO  L87              Difference]: Start difference. First operand  has 42 states, 17 states have (on average 1.3529411764705883) internal successors, (23), 23 states have internal predecessors, (23), 15 states have call successors, (15), 8 states have call predecessors, (15), 8 states have return successors, (15), 11 states have call predecessors, (15), 15 states have call successors, (15) Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:38,679 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,679 INFO  L93              Difference]: Finished difference Result 42 states and 54 transitions.
[2025-04-28 21:21:38,681 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:38,683 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 20
[2025-04-28 21:21:38,683 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,692 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:38,692 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:38,694 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:38,698 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 1 mSDsluCounter, 87 mSDsCounter, 0 mSdLazyCounter, 12 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 136 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 12 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,700 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 136 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 12 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:38,724 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:38,794 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 42.
[2025-04-28 21:21:38,795 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 17 states have (on average 1.2941176470588236) internal successors, (22), 22 states have internal predecessors, (22), 15 states have call successors, (15), 8 states have call predecessors, (15), 9 states have return successors, (17), 11 states have call predecessors, (17), 15 states have call successors, (17)
[2025-04-28 21:21:38,810 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 54 transitions.
[2025-04-28 21:21:38,811 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 54 transitions. Word has length 20
[2025-04-28 21:21:38,812 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,812 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 54 transitions.
[2025-04-28 21:21:38,812 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:38,812 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 54 transitions.
[2025-04-28 21:21:38,818 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:38,819 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,819 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,819 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:38,820 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,822 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,822 INFO  L85        PathProgramCache]: Analyzing trace with hash -537493861, now seen corresponding path program 1 times
[2025-04-28 21:21:38,822 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,822 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1031009825]
[2025-04-28 21:21:38,822 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,823 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,858 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:38,937 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:38,937 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,937 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,120 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:39,121 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,121 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1031009825]
[2025-04-28 21:21:39,121 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1031009825] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,121 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,121 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:39,121 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [790220112]
[2025-04-28 21:21:39,121 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,123 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,123 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,124 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,124 INFO  L87              Difference]: Start difference. First operand 42 states and 54 transitions. Second operand  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,177 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,177 INFO  L93              Difference]: Finished difference Result 44 states and 57 transitions.
[2025-04-28 21:21:39,178 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:39,178 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:39,179 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,180 INFO  L225             Difference]: With dead ends: 44
[2025-04-28 21:21:39,180 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:39,180 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:39,181 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 1 mSDsluCounter, 86 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 135 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,181 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 135 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:39,182 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:39,188 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 42.
[2025-04-28 21:21:39,188 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 17 states have (on average 1.2941176470588236) internal successors, (22), 22 states have internal predecessors, (22), 15 states have call successors, (15), 8 states have call predecessors, (15), 9 states have return successors, (17), 12 states have call predecessors, (17), 15 states have call successors, (17)
[2025-04-28 21:21:39,189 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 54 transitions.
[2025-04-28 21:21:39,190 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 54 transitions. Word has length 24
[2025-04-28 21:21:39,190 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,190 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 54 transitions.
[2025-04-28 21:21:39,190 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.0) internal successors, (12), 4 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,191 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 54 transitions.
[2025-04-28 21:21:39,192 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:39,192 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,192 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,192 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:39,192 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,193 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,193 INFO  L85        PathProgramCache]: Analyzing trace with hash 320205137, now seen corresponding path program 1 times
[2025-04-28 21:21:39,193 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,193 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [307965430]
[2025-04-28 21:21:39,194 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,194 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,210 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:39,228 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:39,229 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,229 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,546 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:39,546 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,546 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [307965430]
[2025-04-28 21:21:39,546 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [307965430] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,546 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,546 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:39,546 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1054686410]
[2025-04-28 21:21:39,547 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,547 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:39,547 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,548 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:39,548 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:39,548 INFO  L87              Difference]: Start difference. First operand 42 states and 54 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,704 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,706 INFO  L93              Difference]: Finished difference Result 46 states and 60 transitions.
[2025-04-28 21:21:39,706 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:39,707 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:39,707 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,708 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:39,710 INFO  L226             Difference]: Without dead ends: 46
[2025-04-28 21:21:39,711 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:39,711 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 2 mSDsluCounter, 161 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 207 SdHoareTripleChecker+Invalid, 38 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,712 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 207 Invalid, 38 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:39,713 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-04-28 21:21:39,721 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 42.
[2025-04-28 21:21:39,721 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 17 states have (on average 1.2941176470588236) internal successors, (22), 22 states have internal predecessors, (22), 15 states have call successors, (15), 8 states have call predecessors, (15), 9 states have return successors, (17), 12 states have call predecessors, (17), 15 states have call successors, (17)
[2025-04-28 21:21:39,723 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 54 transitions.
[2025-04-28 21:21:39,725 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 54 transitions. Word has length 24
[2025-04-28 21:21:39,725 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,725 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 54 transitions.
[2025-04-28 21:21:39,726 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:39,726 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 54 transitions.
[2025-04-28 21:21:39,727 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:39,729 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,729 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,729 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:39,729 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,730 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,732 INFO  L85        PathProgramCache]: Analyzing trace with hash 1139938647, now seen corresponding path program 1 times
[2025-04-28 21:21:39,733 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,733 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [596311983]
[2025-04-28 21:21:39,733 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,733 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,758 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:39,798 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:39,802 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,803 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,432 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:40,432 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,432 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [596311983]
[2025-04-28 21:21:40,433 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [596311983] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,433 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1911423289]
[2025-04-28 21:21:40,433 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,433 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,437 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,442 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:40,444 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,543 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:40,624 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:40,624 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,624 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,631 INFO  L256         TraceCheckSpWp]: Trace formula consists of 330 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,638 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,113 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:41,113 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,911 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:42,912 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1911423289] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,912 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,912 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 18
[2025-04-28 21:21:42,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1798986597]
[2025-04-28 21:21:42,912 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,913 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:42,913 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,914 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:42,915 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=49, Invalid=257, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:42,916 INFO  L87              Difference]: Start difference. First operand 42 states and 54 transitions. Second operand  has 18 states, 7 states have (on average 3.4285714285714284) internal successors, (24), 15 states have internal predecessors, (24), 14 states have call successors, (19), 1 states have call predecessors, (19), 7 states have return successors, (19), 11 states have call predecessors, (19), 14 states have call successors, (19)
[2025-04-28 21:21:43,509 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,509 INFO  L93              Difference]: Finished difference Result 47 states and 65 transitions.
[2025-04-28 21:21:43,510 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:43,510 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 7 states have (on average 3.4285714285714284) internal successors, (24), 15 states have internal predecessors, (24), 14 states have call successors, (19), 1 states have call predecessors, (19), 7 states have return successors, (19), 11 states have call predecessors, (19), 14 states have call successors, (19) Word has length 36
[2025-04-28 21:21:43,511 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,512 INFO  L225             Difference]: With dead ends: 47
[2025-04-28 21:21:43,512 INFO  L226             Difference]: Without dead ends: 47
[2025-04-28 21:21:43,512 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 89 GetRequests, 66 SyntacticMatches, 1 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 48 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=94, Invalid=458, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:43,513 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 8 mSDsluCounter, 547 mSDsCounter, 0 mSdLazyCounter, 198 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 593 SdHoareTripleChecker+Invalid, 225 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 198 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,514 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 593 Invalid, 225 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 198 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:43,515 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 47 states.
[2025-04-28 21:21:43,520 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 47 to 45.
[2025-04-28 21:21:43,520 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 18 states have (on average 1.2777777777777777) internal successors, (23), 23 states have internal predecessors, (23), 16 states have call successors, (16), 8 states have call predecessors, (16), 10 states have return successors, (22), 13 states have call predecessors, (22), 16 states have call successors, (22)
[2025-04-28 21:21:43,521 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 61 transitions.
[2025-04-28 21:21:43,522 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 61 transitions. Word has length 36
[2025-04-28 21:21:43,522 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,522 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 61 transitions.
[2025-04-28 21:21:43,522 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 7 states have (on average 3.4285714285714284) internal successors, (24), 15 states have internal predecessors, (24), 14 states have call successors, (19), 1 states have call predecessors, (19), 7 states have return successors, (19), 11 states have call predecessors, (19), 14 states have call successors, (19)
[2025-04-28 21:21:43,522 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 61 transitions.
[2025-04-28 21:21:43,524 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:43,524 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,524 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,531 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:43,725 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,725 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,726 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,726 INFO  L85        PathProgramCache]: Analyzing trace with hash 1436414867, now seen corresponding path program 1 times
[2025-04-28 21:21:43,726 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,726 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1921388305]
[2025-04-28 21:21:43,727 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,727 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,741 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:43,756 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:43,756 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,756 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,012 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 4 proven. 4 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:44,012 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,012 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1921388305]
[2025-04-28 21:21:44,012 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1921388305] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,012 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1953313637]
[2025-04-28 21:21:44,012 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,012 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,016 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,018 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:44,023 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,102 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:44,163 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:44,163 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,163 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,165 INFO  L256         TraceCheckSpWp]: Trace formula consists of 368 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,168 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,563 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 4 proven. 4 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:44,564 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,100 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 4 proven. 4 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:46,101 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1953313637] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,101 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,101 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:21:46,102 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2107768727]
[2025-04-28 21:21:46,102 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,102 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:46,102 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,103 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:46,105 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=408, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:46,105 INFO  L87              Difference]: Start difference. First operand 45 states and 61 transitions. Second operand  has 22 states, 10 states have (on average 3.4) internal successors, (34), 18 states have internal predecessors, (34), 14 states have call successors, (23), 1 states have call predecessors, (23), 10 states have return successors, (23), 12 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:46,773 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,773 INFO  L93              Difference]: Finished difference Result 54 states and 78 transitions.
[2025-04-28 21:21:46,774 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:46,774 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 3.4) internal successors, (34), 18 states have internal predecessors, (34), 14 states have call successors, (23), 1 states have call predecessors, (23), 10 states have return successors, (23), 12 states have call predecessors, (23), 14 states have call successors, (23) Word has length 40
[2025-04-28 21:21:46,774 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,776 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:46,776 INFO  L226             Difference]: Without dead ends: 53
[2025-04-28 21:21:46,777 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 102 GetRequests, 71 SyntacticMatches, 1 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 67 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=132, Invalid=860, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:46,778 INFO  L437           NwaCegarLoop]: 47 mSDtfsCounter, 10 mSDsluCounter, 708 mSDsCounter, 0 mSdLazyCounter, 265 mSolverCounterSat, 33 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 755 SdHoareTripleChecker+Invalid, 298 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 33 IncrementalHoareTripleChecker+Valid, 265 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,778 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 755 Invalid, 298 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [33 Valid, 265 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:46,779 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 53 states.
[2025-04-28 21:21:46,786 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 53 to 49.
[2025-04-28 21:21:46,786 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 49 states, 20 states have (on average 1.25) internal successors, (25), 25 states have internal predecessors, (25), 16 states have call successors, (16), 8 states have call predecessors, (16), 12 states have return successors, (27), 15 states have call predecessors, (27), 16 states have call successors, (27)
[2025-04-28 21:21:46,787 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 49 states to 49 states and 68 transitions.
[2025-04-28 21:21:46,788 INFO  L79                 Accepts]: Start accepts. Automaton has 49 states and 68 transitions. Word has length 40
[2025-04-28 21:21:46,788 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,788 INFO  L485      AbstractCegarLoop]: Abstraction has 49 states and 68 transitions.
[2025-04-28 21:21:46,788 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 3.4) internal successors, (34), 18 states have internal predecessors, (34), 14 states have call successors, (23), 1 states have call predecessors, (23), 10 states have return successors, (23), 12 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:46,788 INFO  L278                IsEmpty]: Start isEmpty. Operand 49 states and 68 transitions.
[2025-04-28 21:21:46,790 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:46,790 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,791 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,799 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:46,993 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,993 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,993 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,993 INFO  L85        PathProgramCache]: Analyzing trace with hash -1085190139, now seen corresponding path program 1 times
[2025-04-28 21:21:46,994 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,994 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1665744221]
[2025-04-28 21:21:46,994 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,994 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,012 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:47,026 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:47,026 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,026 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,274 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 4 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:47,274 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,274 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1665744221]
[2025-04-28 21:21:47,274 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1665744221] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,274 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1472701887]
[2025-04-28 21:21:47,275 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,275 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,277 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,280 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:47,284 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,377 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:47,441 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:47,441 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,441 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,445 INFO  L256         TraceCheckSpWp]: Trace formula consists of 406 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,450 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,708 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 4 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:47,708 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,906 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 4 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:48,906 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1472701887] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,907 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,907 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 8, 8] total 19
[2025-04-28 21:21:48,907 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2001653852]
[2025-04-28 21:21:48,907 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,907 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:48,908 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,908 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:48,909 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:48,909 INFO  L87              Difference]: Start difference. First operand 49 states and 68 transitions. Second operand  has 19 states, 9 states have (on average 3.5555555555555554) internal successors, (32), 17 states have internal predecessors, (32), 13 states have call successors, (22), 1 states have call predecessors, (22), 9 states have return successors, (23), 11 states have call predecessors, (23), 13 states have call successors, (23)
[2025-04-28 21:21:49,351 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,352 INFO  L93              Difference]: Finished difference Result 46 states and 67 transitions.
[2025-04-28 21:21:49,352 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:49,352 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 3.5555555555555554) internal successors, (32), 17 states have internal predecessors, (32), 13 states have call successors, (22), 1 states have call predecessors, (22), 9 states have return successors, (23), 11 states have call predecessors, (23), 13 states have call successors, (23) Word has length 44
[2025-04-28 21:21:49,353 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,353 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:49,353 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:49,353 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 111 GetRequests, 82 SyntacticMatches, 1 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 67 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=122, Invalid=748, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:49,354 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 6 mSDsluCounter, 516 mSDsCounter, 0 mSdLazyCounter, 199 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 558 SdHoareTripleChecker+Invalid, 224 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 199 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,354 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 558 Invalid, 224 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 199 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,355 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:49,355 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:49,355 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:49,355 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:49,355 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 44
[2025-04-28 21:21:49,355 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,356 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:49,356 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 3.5555555555555554) internal successors, (32), 17 states have internal predecessors, (32), 13 states have call successors, (22), 1 states have call predecessors, (22), 9 states have return successors, (23), 11 states have call predecessors, (23), 13 states have call successors, (23)
[2025-04-28 21:21:49,356 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:49,356 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:49,358 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:49,365 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:49,563 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,566 INFO  L422         BasicCegarLoop]: Path program histogram: [1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,568 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:49,572 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:49 BoogieIcfgContainer
[2025-04-28 21:21:49,572 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:49,573 INFO  L158              Benchmark]: Toolchain (without parser) took 12137.10ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 161.4MB in the beginning and 57.9MB in the end (delta: 103.5MB). Peak memory consumption was 29.1MB. Max. memory is 33.6GB.
[2025-04-28 21:21:49,573 INFO  L158              Benchmark]: SmtParser took 1.60ms. Allocated memory is still 234.9MB. Free memory is still 172.0MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:49,573 INFO  L158              Benchmark]: ChcToBoogie took 58.09ms. Allocated memory is still 234.9MB. Free memory was 160.7MB in the beginning and 159.9MB in the end (delta: 755.0kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:49,573 INFO  L158              Benchmark]: Boogie Preprocessor took 96.50ms. Allocated memory is still 234.9MB. Free memory was 159.9MB in the beginning and 157.6MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:49,574 INFO  L158              Benchmark]: RCFGBuilder took 486.84ms. Allocated memory is still 234.9MB. Free memory was 157.6MB in the beginning and 142.0MB in the end (delta: 15.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:49,574 INFO  L158              Benchmark]: TraceAbstraction took 11486.61ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 142.0MB in the beginning and 57.9MB in the end (delta: 84.1MB). Peak memory consumption was 12.4MB. Max. memory is 33.6GB.
[2025-04-28 21:21:49,576 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 1.60ms. Allocated memory is still 234.9MB. Free memory is still 172.0MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 58.09ms. Allocated memory is still 234.9MB. Free memory was 160.7MB in the beginning and 159.9MB in the end (delta: 755.0kB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 96.50ms. Allocated memory is still 234.9MB. Free memory was 159.9MB in the beginning and 157.6MB in the end (delta: 2.3MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 486.84ms. Allocated memory is still 234.9MB. Free memory was 157.6MB in the beginning and 142.0MB in the end (delta: 15.6MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 11486.61ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 142.0MB in the beginning and 57.9MB in the end (delta: 84.1MB). Peak memory consumption was 12.4MB. 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 9 procedures, 42 locations, 68 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 11.4s, OverallIterations: 6, TraceHistogramMax: 3, PathProgramHistogramMax: 1, EmptinessCheckTime: 0.0s, AutomataDifference: 2.1s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 35 SdHoareTripleChecker+Valid, 1.0s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 28 mSDsluCounter, 2384 SdHoareTripleChecker+Invalid, 0.9s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 2105 mSDsCounter, 89 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 720 IncrementalHoareTripleChecker+Invalid, 809 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 89 mSolverCounterUnsat, 279 mSDtfsCounter, 720 mSolverCounterSat, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 317 GetRequests, 225 SyntacticMatches, 3 SemanticMatches, 89 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 182 ImplicationChecksByTransitivity, 2.0s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=49occurred in iteration=5, InterpolantAutomatonStates: 55, 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, 6 MinimizatonAttempts, 12 StatesRemovedByMinimization, 4 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.4s SatisfiabilityAnalysisTime, 7.5s InterpolantComputationTime, 308 NumberOfCodeBlocks, 308 NumberOfCodeBlocksAsserted, 9 NumberOfCheckSat, 416 ConstructedInterpolants, 0 QuantifiedInterpolants, 1120 SizeOfPredicates, 31 NumberOfNonLiveVariables, 1104 ConjunctsInSsa, 46 ConjunctsInUnsatCore, 12 InterpolantComputations, 3 PerfectInterpolantSequences, 81/117 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:49,596 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
