diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2016-01-01 12:30:04 -0800 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-01-01 12:30:04 -0800 |
| commit | 541c88a37f0880d7ea42a1aaa3a8688fc86ac811 (patch) | |
| tree | d472c4ce579a1a52cb55d33fa1c7f45ec93455fd /src/theory/uf | |
| parent | 395e05c2c443845c71dd1fdbb3eae26a68f15520 (diff) | |
Added propagation rule for array ext lemmas to aid proofs
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/equality_engine_types.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index d91d5e4f2..fb1e73575 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -74,6 +74,7 @@ enum MergeReasonType { /** Theory specific proof rules */ MERGED_ARRAYS_ROW, MERGED_ARRAYS_ROW1, + MERGED_ARRAYS_EXT }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { |