projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4745737) | patch
In a ROW guard proof, if the transitivity proof does not have a disequality, we can...
authorguykatzz <katz911@gmail.com>
Sat, 17 Sep 2016 00:18:56 +0000 (17:18 -0700)
committerguykatzz <katz911@gmail.com>
Sat, 17 Sep 2016 00:18:56 +0000 (17:18 -0700)
commit53d625529c90c81b46a08811e4143552095fff9a
tree4c7359c2a9af6d35d6c64b2a09876b12f302108etree
parent4745737174f9d48e68aa59823f25c0b3ce31cc3ccommit | diff
In a ROW guard proof, if the transitivity proof does not have a disequality, we can deduce that it is a constant-disequality proof and process it accordingly
src/theory/arrays/array_proof_reconstruction.cpp diff | blob | history