projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75d1a09) | patch
Change output of abduction/interpolation for failed inputs (#8396)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Mar 2022 19:19:35 +0000 (14:19 -0500)
committerGitHub <noreply@github.com>
Fri, 25 Mar 2022 19:19:35 +0000 (19:19 +0000)
commit219e2763d670e7bad8d6178fa4dd80b5bf1f6ea8
tree221e3d16892625890ae3843071648378fe8d7b29tree
parent75d1a09f9d797cc3449e1a922e978d21e50f4b15commit | diff
Change output of abduction/interpolation for failed inputs (#8396)

Changes from "none" to "fail" to be consistent with SyGuS standard. Note that this means that we don't know if an abduct/interpolant exists.
src/smt/command.cpp diff | blob | history
test/regress/cli/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 diff | blob | history
test/regress/cli/regress1/abduction/issue5848-4.smt2 diff | blob | history