projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7f84ff8) | patch
Fix type checking for define-funs (resolves bug 398).
authorMorgan Deters <mdeters@gmail.com>
Wed, 26 Sep 2012 03:50:57 +0000 (03:50 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 26 Sep 2012 03:50:57 +0000 (03:50 +0000)
commited914e42041806538f57750c8391fa77053d8c79
treed6da32187d9bab77bef2a5e483f2065c7adbdb98tree
parent7f84ff856af53047c2af2c1c1987340f9075ec7ccommit | diff
Fix type checking for define-funs (resolves bug 398).

(this commit was certified error- and warning-free by the test-and-commit script.)
src/smt/smt_engine.cpp diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history