projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c7f50a0) | patch
Fix non-parametrized operators in subgoal generation (#4023)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Mar 2020 17:18:59 +0000 (12:18 -0500)
committerGitHub <noreply@github.com>
Wed, 11 Mar 2020 17:18:59 +0000 (12:18 -0500)
commitac5ef49e14154daee4200783b57584febb726a4e
treeeaab7a14b8a734f0a017595ea7de56487875690btree
parentc7f50a009cad7a0c1a2f1a5290e1d7bd03edf0e7commit | diff
Fix non-parametrized operators in subgoal generation (#4023)

Fixes #4021.

We were previously constructing a malformed HO_APPLY as part of a subgoal for induction.
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 [new file with mode: 0644] blob