projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 73a9276) | patch
Fix remaining synthesis solution regressions (#1557)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 2 Feb 2018 23:20:44 +0000 (17:20 -0600)
committerGitHub <noreply@github.com>
Fri, 2 Feb 2018 23:20:44 +0000 (17:20 -0600)
commitae5c1a5c3a9c6eb7d1af1a4ddbcb841cf7ce4c70
tree3d8fe399ff6a6dd6ac7cf119b422cc1d5ea5604dtree
parent73a92766063e76e6c6f2507f126fb8f84ed3e432commit | diff
Fix remaining synthesis solution regressions (#1557)
src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv_sol.h diff | blob | history
src/theory/quantifiers/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/term_database_sygus.h diff | blob | history
test/regress/regress0/sygus/General_plus10.sy diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/array_search_2.sy diff | blob | history
test/regress/regress0/sygus/c100.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/const-var-test.sy diff | blob | history
test/regress/regress0/sygus/max.sy diff | blob | history