projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 976ee5b) | patch
Handling a corner case where a ROW's guard is a constant disequality.
authorGuy <guy@Guy-X260>
Fri, 16 Sep 2016 23:26:30 +0000 (16:26 -0700)
committerGuy <guy@Guy-X260>
Fri, 16 Sep 2016 23:26:30 +0000 (16:26 -0700)
commit0e68cfe050946d1ed9544dffcbd5e75be0e6f22f
tree1c968358d3ff2f5bc592a89ca52d2c5f91fdb54ftree
parent976ee5b66b7584b9fe46eab1facf5e5f857e723fcommit | diff
Handling a corner case where a ROW's guard is a constant disequality.
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
src/theory/arrays/array_proof_reconstruction.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history