projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f0f35c) | patch
disallow assertions to inactive theories.
authorMorgan Deters <mdeters@gmail.com>
Fri, 24 Aug 2012 23:20:22 +0000 (23:20 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 24 Aug 2012 23:20:22 +0000 (23:20 +0000)
commit3619c784bd5dd4b91ab0a2ad429ea145636d3424
tree746cf2326c4fd279b89e019ff0131f9ef9867b65tree
parent5f0f35cc281b988db6d0f3dfa4b797f91b69f6abcommit | diff
disallow assertions to inactive theories.

this fixes at least one known bug where quantifiers could be asserted in quantifier-free logics, with incorrect results.
src/theory/theory_engine.cpp diff | blob | history