./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-212.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:38,275 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:38,361 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_299a0124-df22-49cb-91a5-acfd9da963d1/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:38,366 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:38,366 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:38,392 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:38,393 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:38,393 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:38,393 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:38,393 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:38,394 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:38,394 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:38,394 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:38,394 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:38,394 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:38,394 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:38,394 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:38,395 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:38,395 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:38,396 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:38,396 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:38,719 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:38,730 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:38,733 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:38,735 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:38,735 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:38,738 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_299a0124-df22-49cb-91a5-acfd9da963d1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-212.smt2
[2025-04-28 21:21:38,740 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:38,746 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:39,770 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_299a0124-df22-49cb-91a5-acfd9da963d1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-212.smt2
[2025-04-28 21:21:39,774 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:39,777 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:39,778 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:39,778 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:39,778 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:39,781 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,889 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39 Unit
[2025-04-28 21:21:39,890 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:39,891 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:39,892 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:39,892 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:39,910 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,911 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,967 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,967 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:39,997 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:40,000 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:40,003 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:40,013 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:40,020 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:40,053 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,054 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:40,054 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:40,054 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:40,055 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (1/1) ...
[2025-04-28 21:21:40,058 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,072 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,091 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:40,098 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:40,112 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:40,112 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:40,113 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:40,113 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:40,113 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:40,113 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:40,114 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn__bar given in one single declaration
[2025-04-28 21:21:40,114 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn__bar
[2025-04-28 21:21:40,114 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn__bar
[2025-04-28 21:21:40,114 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn__bar given in one single declaration
[2025-04-28 21:21:40,114 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn__bar
[2025-04-28 21:21:40,114 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn__bar
[2025-04-28 21:21:40,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn given in one single declaration
[2025-04-28 21:21:40,115 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn
[2025-04-28 21:21:40,115 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn
[2025-04-28 21:21:40,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn given in one single declaration
[2025-04-28 21:21:40,115 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn
[2025-04-28 21:21:40,115 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn
[2025-04-28 21:21:40,116 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lturn given in one single declaration
[2025-04-28 21:21:40,116 INFO  L130     BoogieDeclarations]: Found specification of procedure lturn
[2025-04-28 21:21:40,117 INFO  L138     BoogieDeclarations]: Found implementation of procedure lturn
[2025-04-28 21:21:40,117 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:40,117 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:40,117 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:40,245 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:40,248 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,849 INFO  L?                        ?]: Removed 4 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,849 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:41,873 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:41,874 INFO  L312             CfgBuilder]: Removed 12 assume(true) statements.
[2025-04-28 21:21:41,874 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41 BoogieIcfgContainer
[2025-04-28 21:21:41,874 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:41,879 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:41,879 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:41,883 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:41,883 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:39" (1/3) ...
[2025-04-28 21:21:41,884 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@34dc4de4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,884 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:39" (2/3) ...
[2025-04-28 21:21:41,885 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@34dc4de4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,885 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41" (3/3) ...
[2025-04-28 21:21:41,886 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:41,902 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:41,905 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 150 locations, 454 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:41,967 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:41,979 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;@69935edf, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:41,980 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:41,986 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 150 states, 13 states have (on average 3.3076923076923075) internal successors, (43), 38 states have internal predecessors, (43), 131 states have call successors, (137), 7 states have call predecessors, (137), 7 states have return successors, (137), 105 states have call predecessors, (137), 131 states have call successors, (137)
[2025-04-28 21:21:42,031 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:42,031 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,032 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,032 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,039 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,039 INFO  L85        PathProgramCache]: Analyzing trace with hash -3696079, now seen corresponding path program 1 times
[2025-04-28 21:21:42,048 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,049 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [857655315]
[2025-04-28 21:21:42,049 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,050 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,118 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:42,345 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:42,346 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,346 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,128 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:43,128 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,129 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [857655315]
[2025-04-28 21:21:43,129 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [857655315] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,129 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,132 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:43,134 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [799584355]
[2025-04-28 21:21:43,135 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,140 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:43,141 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,192 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:43,193 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,201 INFO  L87              Difference]: Start difference. First operand  has 150 states, 13 states have (on average 3.3076923076923075) internal successors, (43), 38 states have internal predecessors, (43), 131 states have call successors, (137), 7 states have call predecessors, (137), 7 states have return successors, (137), 105 states have call predecessors, (137), 131 states have call successors, (137) Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:45,021 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,021 INFO  L93              Difference]: Finished difference Result 190 states and 522 transitions.
[2025-04-28 21:21:45,023 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,024 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:45,025 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,043 INFO  L225             Difference]: With dead ends: 190
[2025-04-28 21:21:45,043 INFO  L226             Difference]: Without dead ends: 190
[2025-04-28 21:21:45,045 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:45,052 INFO  L437           NwaCegarLoop]: 270 mSDtfsCounter, 9 mSDsluCounter, 941 mSDsCounter, 0 mSdLazyCounter, 706 mSolverCounterSat, 23 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 54 SdHoareTripleChecker+Valid, 1211 SdHoareTripleChecker+Invalid, 729 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 23 IncrementalHoareTripleChecker+Valid, 706 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,055 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [54 Valid, 1211 Invalid, 729 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [23 Valid, 706 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:21:45,073 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 190 states.
[2025-04-28 21:21:45,278 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 190 to 188.
[2025-04-28 21:21:45,280 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 188 states, 15 states have (on average 3.7333333333333334) internal successors, (56), 47 states have internal predecessors, (56), 167 states have call successors, (174), 9 states have call predecessors, (174), 9 states have return successors, (289), 133 states have call predecessors, (289), 167 states have call successors, (289)
[2025-04-28 21:21:45,290 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 188 states to 188 states and 519 transitions.
[2025-04-28 21:21:45,291 INFO  L79                 Accepts]: Start accepts. Automaton has 188 states and 519 transitions. Word has length 18
[2025-04-28 21:21:45,294 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,294 INFO  L485      AbstractCegarLoop]: Abstraction has 188 states and 519 transitions.
[2025-04-28 21:21:45,295 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:45,295 INFO  L278                IsEmpty]: Start isEmpty. Operand 188 states and 519 transitions.
[2025-04-28 21:21:45,310 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:45,310 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,310 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,310 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,310 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,312 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,312 INFO  L85        PathProgramCache]: Analyzing trace with hash -789750099, now seen corresponding path program 1 times
[2025-04-28 21:21:45,312 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,312 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2127167637]
[2025-04-28 21:21:45,312 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,312 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,342 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:45,407 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:45,408 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,409 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,089 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:46,089 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,089 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2127167637]
[2025-04-28 21:21:46,090 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2127167637] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,090 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,090 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:46,090 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [846694535]
[2025-04-28 21:21:46,090 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,092 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:46,094 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,095 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:46,095 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,095 INFO  L87              Difference]: Start difference. First operand 188 states and 519 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:47,464 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,464 INFO  L93              Difference]: Finished difference Result 270 states and 1022 transitions.
[2025-04-28 21:21:47,464 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:47,465 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:47,465 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,476 INFO  L225             Difference]: With dead ends: 270
[2025-04-28 21:21:47,477 INFO  L226             Difference]: Without dead ends: 270
[2025-04-28 21:21:47,477 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:47,478 INFO  L437           NwaCegarLoop]: 290 mSDtfsCounter, 10 mSDsluCounter, 1030 mSDsCounter, 0 mSdLazyCounter, 646 mSolverCounterSat, 33 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 52 SdHoareTripleChecker+Valid, 1320 SdHoareTripleChecker+Invalid, 679 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 33 IncrementalHoareTripleChecker+Valid, 646 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,478 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [52 Valid, 1320 Invalid, 679 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [33 Valid, 646 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:47,480 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 270 states.
[2025-04-28 21:21:47,662 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 270 to 268.
[2025-04-28 21:21:47,663 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 268 states, 21 states have (on average 3.761904761904762) internal successors, (79), 68 states have internal predecessors, (79), 239 states have call successors, (249), 13 states have call predecessors, (249), 13 states have return successors, (692), 189 states have call predecessors, (692), 239 states have call successors, (692)
[2025-04-28 21:21:47,671 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 268 states to 268 states and 1020 transitions.
[2025-04-28 21:21:47,671 INFO  L79                 Accepts]: Start accepts. Automaton has 268 states and 1020 transitions. Word has length 18
[2025-04-28 21:21:47,671 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,672 INFO  L485      AbstractCegarLoop]: Abstraction has 268 states and 1020 transitions.
[2025-04-28 21:21:47,672 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:47,672 INFO  L278                IsEmpty]: Start isEmpty. Operand 268 states and 1020 transitions.
[2025-04-28 21:21:47,681 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:47,681 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,682 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,682 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:47,682 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,683 INFO  L85        PathProgramCache]: Analyzing trace with hash 985335563, now seen corresponding path program 1 times
[2025-04-28 21:21:47,684 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,684 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [419178080]
[2025-04-28 21:21:47,684 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,717 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:47,757 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:47,758 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,758 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,468 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:48,468 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,468 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [419178080]
[2025-04-28 21:21:48,468 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [419178080] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,468 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,468 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:48,468 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [35677069]
[2025-04-28 21:21:48,469 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,469 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,469 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,469 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,469 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,470 INFO  L87              Difference]: Start difference. First operand 268 states and 1020 transitions. Second operand  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:50,030 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,030 INFO  L93              Difference]: Finished difference Result 317 states and 1451 transitions.
[2025-04-28 21:21:50,030 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:50,031 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:50,031 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,046 INFO  L225             Difference]: With dead ends: 317
[2025-04-28 21:21:50,046 INFO  L226             Difference]: Without dead ends: 317
[2025-04-28 21:21:50,046 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,047 INFO  L437           NwaCegarLoop]: 327 mSDtfsCounter, 9 mSDsluCounter, 1097 mSDsCounter, 0 mSdLazyCounter, 939 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 40 SdHoareTripleChecker+Valid, 1424 SdHoareTripleChecker+Invalid, 969 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 939 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,047 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [40 Valid, 1424 Invalid, 969 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 939 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:50,048 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 317 states.
[2025-04-28 21:21:50,284 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 317 to 314.
[2025-04-28 21:21:50,286 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 314 states, 27 states have (on average 3.4074074074074074) internal successors, (92), 81 states have internal predecessors, (92), 275 states have call successors, (287), 15 states have call predecessors, (287), 18 states have return successors, (1069), 220 states have call predecessors, (1069), 275 states have call successors, (1069)
[2025-04-28 21:21:50,297 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 314 states to 314 states and 1448 transitions.
[2025-04-28 21:21:50,298 INFO  L79                 Accepts]: Start accepts. Automaton has 314 states and 1448 transitions. Word has length 21
[2025-04-28 21:21:50,298 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,298 INFO  L485      AbstractCegarLoop]: Abstraction has 314 states and 1448 transitions.
[2025-04-28 21:21:50,299 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:50,299 INFO  L278                IsEmpty]: Start isEmpty. Operand 314 states and 1448 transitions.
[2025-04-28 21:21:50,314 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:50,314 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,314 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,316 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:50,316 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,317 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,321 INFO  L85        PathProgramCache]: Analyzing trace with hash -2003290362, now seen corresponding path program 1 times
[2025-04-28 21:21:50,321 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,321 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1070104087]
[2025-04-28 21:21:50,321 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,322 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,343 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:50,375 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:50,375 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,375 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,895 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:50,895 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,896 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1070104087]
[2025-04-28 21:21:50,896 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1070104087] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,896 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,896 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:50,896 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1945423998]
[2025-04-28 21:21:50,896 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,896 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:50,896 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,897 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:50,897 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,897 INFO  L87              Difference]: Start difference. First operand 314 states and 1448 transitions. Second operand  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:52,221 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,221 INFO  L93              Difference]: Finished difference Result 447 states and 2892 transitions.
[2025-04-28 21:21:52,221 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:52,222 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:52,222 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,241 INFO  L225             Difference]: With dead ends: 447
[2025-04-28 21:21:52,241 INFO  L226             Difference]: Without dead ends: 447
[2025-04-28 21:21:52,241 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:52,242 INFO  L437           NwaCegarLoop]: 367 mSDtfsCounter, 9 mSDsluCounter, 1303 mSDsCounter, 0 mSdLazyCounter, 730 mSolverCounterSat, 29 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 44 SdHoareTripleChecker+Valid, 1670 SdHoareTripleChecker+Invalid, 759 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 29 IncrementalHoareTripleChecker+Valid, 730 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,242 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [44 Valid, 1670 Invalid, 759 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [29 Valid, 730 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:21:52,244 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 447 states.
[2025-04-28 21:21:52,841 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 447 to 442.
[2025-04-28 21:21:52,843 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 442 states, 40 states have (on average 2.975) internal successors, (119), 108 states have internal predecessors, (119), 381 states have call successors, (397), 19 states have call predecessors, (397), 29 states have return successors, (2362), 317 states have call predecessors, (2362), 381 states have call successors, (2362)
[2025-04-28 21:21:52,860 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 442 states to 442 states and 2878 transitions.
[2025-04-28 21:21:52,861 INFO  L79                 Accepts]: Start accepts. Automaton has 442 states and 2878 transitions. Word has length 21
[2025-04-28 21:21:52,861 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,861 INFO  L485      AbstractCegarLoop]: Abstraction has 442 states and 2878 transitions.
[2025-04-28 21:21:52,861 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:52,861 INFO  L278                IsEmpty]: Start isEmpty. Operand 442 states and 2878 transitions.
[2025-04-28 21:21:52,874 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:52,874 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,875 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,875 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:52,875 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,875 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,876 INFO  L85        PathProgramCache]: Analyzing trace with hash -1667078427, now seen corresponding path program 1 times
[2025-04-28 21:21:52,876 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,876 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1948462423]
[2025-04-28 21:21:52,876 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,876 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,896 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:52,941 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:52,941 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,941 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,450 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:53,451 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,451 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1948462423]
[2025-04-28 21:21:53,451 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1948462423] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,451 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [814398919]
[2025-04-28 21:21:53,451 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,451 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,454 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,458 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:53,460 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,528 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:53,676 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:53,676 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,676 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,683 INFO  L256         TraceCheckSpWp]: Trace formula consists of 932 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,690 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,764 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:53,764 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,534 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:54,534 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [814398919] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,534 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,535 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 11
[2025-04-28 21:21:54,535 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1727282899]
[2025-04-28 21:21:54,535 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,535 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:54,535 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,536 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:54,536 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=88, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:54,536 INFO  L87              Difference]: Start difference. First operand 442 states and 2878 transitions. Second operand  has 11 states, 9 states have (on average 1.4444444444444444) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 8 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:58,373 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,374 INFO  L93              Difference]: Finished difference Result 861 states and 10525 transitions.
[2025-04-28 21:21:58,374 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:58,374 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 9 states have (on average 1.4444444444444444) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 8 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10) Word has length 24
[2025-04-28 21:21:58,375 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,478 INFO  L225             Difference]: With dead ends: 861
[2025-04-28 21:21:58,479 INFO  L226             Difference]: Without dead ends: 861
[2025-04-28 21:21:58,479 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 43 SyntacticMatches, 3 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 6 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=88, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:58,482 INFO  L437           NwaCegarLoop]: 317 mSDtfsCounter, 34 mSDsluCounter, 2163 mSDsCounter, 0 mSdLazyCounter, 2805 mSolverCounterSat, 97 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 3.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 143 SdHoareTripleChecker+Valid, 2480 SdHoareTripleChecker+Invalid, 2902 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 97 IncrementalHoareTripleChecker+Valid, 2805 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,483 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [143 Valid, 2480 Invalid, 2902 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [97 Valid, 2805 Invalid, 0 Unknown, 0 Unchecked, 3.6s Time]
[2025-04-28 21:21:58,485 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 861 states.
[2025-04-28 21:22:00,535 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 861 to 848.
[2025-04-28 21:22:00,543 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 848 states, 79 states have (on average 2.759493670886076) internal successors, (218), 193 states have internal predecessors, (218), 721 states have call successors, (745), 31 states have call predecessors, (745), 62 states have return successors, (9490), 630 states have call predecessors, (9490), 721 states have call successors, (9490)
[2025-04-28 21:22:00,596 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 848 states to 848 states and 10453 transitions.
[2025-04-28 21:22:00,597 INFO  L79                 Accepts]: Start accepts. Automaton has 848 states and 10453 transitions. Word has length 24
[2025-04-28 21:22:00,597 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,597 INFO  L485      AbstractCegarLoop]: Abstraction has 848 states and 10453 transitions.
[2025-04-28 21:22:00,597 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 9 states have (on average 1.4444444444444444) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (8), 1 states have call predecessors, (8), 8 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:00,597 INFO  L278                IsEmpty]: Start isEmpty. Operand 848 states and 10453 transitions.
[2025-04-28 21:22:00,624 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:00,624 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,624 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]
[2025-04-28 21:22:00,632 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:22:00,826 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:22:00,826 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,829 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,829 INFO  L85        PathProgramCache]: Analyzing trace with hash 1725599309, now seen corresponding path program 1 times
[2025-04-28 21:22:00,829 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,829 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [620634181]
[2025-04-28 21:22:00,829 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,829 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,850 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:00,881 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:00,881 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,881 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,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:22:01,120 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,120 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [620634181]
[2025-04-28 21:22:01,121 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [620634181] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,121 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:01,121 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:22:01,121 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2085289516]
[2025-04-28 21:22:01,121 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,121 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:22:01,123 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:22:01,124 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:22:01,124 INFO  L87              Difference]: Start difference. First operand 848 states and 10453 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:22:02,745 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,745 INFO  L93              Difference]: Finished difference Result 868 states and 11041 transitions.
[2025-04-28 21:22:02,746 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:22:02,746 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:22:02,746 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,807 INFO  L225             Difference]: With dead ends: 868
[2025-04-28 21:22:02,807 INFO  L226             Difference]: Without dead ends: 868
[2025-04-28 21:22:02,807 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-04-28 21:22:02,808 INFO  L437           NwaCegarLoop]: 285 mSDtfsCounter, 9 mSDsluCounter, 1242 mSDsCounter, 0 mSdLazyCounter, 1068 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 57 SdHoareTripleChecker+Valid, 1527 SdHoareTripleChecker+Invalid, 1096 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 1068 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,808 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [57 Valid, 1527 Invalid, 1096 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 1068 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:22:02,810 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 868 states.
[2025-04-28 21:22:04,531 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 868 to 864.
[2025-04-28 21:22:04,539 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 864 states, 82 states have (on average 2.6951219512195124) internal successors, (221), 196 states have internal predecessors, (221), 731 states have call successors, (755), 31 states have call predecessors, (755), 65 states have return successors, (10045), 643 states have call predecessors, (10045), 731 states have call successors, (10045)
[2025-04-28 21:22:04,597 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 864 states to 864 states and 11021 transitions.
[2025-04-28 21:22:04,597 INFO  L79                 Accepts]: Start accepts. Automaton has 864 states and 11021 transitions. Word has length 21
[2025-04-28 21:22:04,597 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,597 INFO  L485      AbstractCegarLoop]: Abstraction has 864 states and 11021 transitions.
[2025-04-28 21:22:04,598 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:22:04,598 INFO  L278                IsEmpty]: Start isEmpty. Operand 864 states and 11021 transitions.
[2025-04-28 21:22:04,625 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:04,626 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,626 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]
[2025-04-28 21:22:04,626 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:22:04,626 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,627 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,627 INFO  L85        PathProgramCache]: Analyzing trace with hash -1451096495, now seen corresponding path program 1 times
[2025-04-28 21:22:04,627 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,627 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2102617915]
[2025-04-28 21:22:04,628 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,628 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,649 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:04,678 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:04,678 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,678 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,025 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:22:05,025 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:05,026 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2102617915]
[2025-04-28 21:22:05,026 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2102617915] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:05,026 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:05,026 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:22:05,027 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1916453560]
[2025-04-28 21:22:05,027 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,027 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:22:05,027 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,028 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:22:05,028 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:22:05,028 INFO  L87              Difference]: Start difference. First operand 864 states and 11021 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:22:06,805 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,805 INFO  L93              Difference]: Finished difference Result 872 states and 11005 transitions.
[2025-04-28 21:22:06,806 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:22:06,806 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:22:06,807 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,856 INFO  L225             Difference]: With dead ends: 872
[2025-04-28 21:22:06,857 INFO  L226             Difference]: Without dead ends: 872
[2025-04-28 21:22:06,857 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-04-28 21:22:06,857 INFO  L437           NwaCegarLoop]: 327 mSDtfsCounter, 10 mSDsluCounter, 1447 mSDsCounter, 0 mSdLazyCounter, 1069 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 61 SdHoareTripleChecker+Valid, 1774 SdHoareTripleChecker+Invalid, 1105 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 1069 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,858 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [61 Valid, 1774 Invalid, 1105 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [36 Valid, 1069 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:22:06,859 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 872 states.
