projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1d4ad74) | patch
When proving a lemma, ignore literals that don't belong to the theory in question...
authorGuy <katz911@gmail.com>
Fri, 1 Jul 2016 23:49:02 +0000 (16:49 -0700)
committerGuy <katz911@gmail.com>
Fri, 1 Jul 2016 23:49:02 +0000 (16:49 -0700)
commita58abbe71fb1fc07129ff9c7568ac544145fb57c
treebbca6289fad9fdd3ea21b27bee9f6be82b1c5685tree
parent1d4ad74ca90641bd9165f9a2c019c54cde6e80c1commit | diff
When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties
src/proof/theory_proof.cpp diff | blob | history