{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:17Z","timestamp":1751660537308},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose infinite model finding as a new task for SMT-Solving. Model finding has a long-standing tradition in SMT and automated reasoning in general. Yet, most of the current tools are limited to finite models despite the fact that many theories only admit infinite models. This paper shows a variety of such problems and evaluates synthesis approaches on them. Interestingly, state-of-the-art SMT solvers fail even on very small and simple problems. We target such problems by SyGuS tools as well as heuristic approaches.<\/jats:p>","DOI":"10.29007\/slrm","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:10Z","timestamp":1685830210000},"page":"317-304","source":"Crossref","is-referenced-by-count":2,"title":["Experiments on Infinite Model Finding in SMT Solving"],"prefix":"10.29007","volume":"94","author":[{"given":"Julian","family":"Parsert","sequence":"first","affiliation":[]},{"given":"Chad","family":"Brown","sequence":"additional","affiliation":[]},{"given":"Mikolas","family":"Janota","sequence":"additional","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:20Z","timestamp":1685830220000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/TLbl"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/slrm","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}