Currently if the stabilization procedure finishes with a cycle in an inclusion, we give unknown if we need to generate model. We should implement the algorithm from the proof in FM'23 (possibly needs to be updated for lengths).
However, only three benchmarks from SMTLIB are cyclic and the stabilization procedure finishes:
Currently if the stabilization procedure finishes with a cycle in an inclusion, we give
unknownif we need to generate model. We should implement the algorithm from the proof in FM'23 (possibly needs to be updated for lengths).However, only three benchmarks from SMTLIB are cyclic and the stabilization procedure finishes:
QF_S/20240318-omark/noodles-unsat-10.smt2QF_SLIA/20230329-woorpje-lu/track05/05_track_169.smt2QF_SLIA/20230329-woorpje-lu/track05/05_track_25.smt2