summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
diff options
context:
space:
mode:
authorGuy <guy@Guy-X260>2016-09-16 16:26:30 -0700
committerGuy <guy@Guy-X260>2016-09-16 16:26:30 -0700
commit0e68cfe050946d1ed9544dffcbd5e75be0e6f22f (patch)
tree1c968358d3ff2f5bc592a89ca52d2c5f91fdb54f /src/theory/quantifiers/quant_conflict_find.cpp
parent976ee5b66b7584b9fe46eab1facf5e5f857e723f (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
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback