projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4cf9134) | patch
Catch cases where recursive functions reference functions-to-synthesize (#6993)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Aug 2021 22:40:05 +0000 (17:40 -0500)
committerGitHub <noreply@github.com>
Thu, 19 Aug 2021 22:40:05 +0000 (22:40 +0000)
commit09719301db1532093117bc60546e01dca77b59b8
tree230245ce4224b5c69df3e8fd19db86298ac76cb6tree
parent4cf91341622270e4aaefe926d4be7fe148c6fa74commit | diff
Catch cases where recursive functions reference functions-to-synthesize (#6993)

We previously incorrectly allowed this, leading to problems that were unsolvable but where we would not warn the user this combination is not supported.

FYI @polgreen
src/smt/assertions.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history