Dear all, thank-you very much for the information you sent on SAT/SMT for termination. That's certainly more than enough for my course at ISR (very short course - I will cover some fundamentals, but for details, I can refer students to this mailing list thread) I cannot give an review of all the answers (I have to read up on some of the papers that were cited, e.g., on incremental SMT solving in NaTT) but just some small observations/comments (Carsten, on AProVE) * improvements via (suitably configured) more modern SAT solvers may be possible. Yes. E.g., Kissat has lots of parameters, and provides a uniform interface (command line and API) My optimizer computed this https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/stra... but the search space is huge, and my optimizer is naive See also https://github.com/arminbiere/kissat/issues/25 There's room for at least one Bachelor's thesis here. * AProVE kills external processes on OS level ... I struggle with this (cf. https://github.com/yav/simple-smt/issues/21) but this may be a Haskell/libraries problem (lazy IO). Stopping Kissat via API just works. (I think it sets some flag that the solver's main loop checks often enough.) (Akihisa, on NaTT) * Coefficients are usually (ite b 0 1) or (ite b 1 2), Interesting! So it's actually a finite-domain constraint. There are classical (non-SMT) solvers for these, e.g. https://www.gecode.org/ Did any-one try this? Possibly via the mini/flatzinc language? https://www.minizinc.org/doc-2.6.4/en/part_4_reference.html Best regards, Johannes.