Fix for corner case of higher-order matching (#1708)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 Apr 2018 21:17:35 +0000 (16:17 -0500)
committerGitHub <noreply@github.com>
Wed, 4 Apr 2018 21:17:35 +0000 (16:17 -0500)
commit0811ba46a8a8818231e7f4e931b99d654c12a348
tree02007a6dfc68675c804babff4a35a7cf271c44f8
parent541b880047374f3748fbf9fa93214bae1308b1aa
Fix for corner case of higher-order matching  (#1708)
src/theory/quantifiers/ematching/ho_trigger.cpp
src/theory/quantifiers/term_database.cpp
test/regress/Makefile.tests
test/regress/regress0/ho/ho-match-fun-suffix.smt2 [new file with mode: 0644]