diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-15 09:48:07 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-15 09:48:07 -0500 |
| commit | 07dd06978875e3275bdebe6bd8495aef34861e8c (patch) | |
| tree | 26b81c151fccdc441df1572943f5ac6dce49e0b1 /src/theory/quantifiers/ceg_instantiator.h | |
| parent | 0369b8325e9f631c77d479e5e9103cdb450bf650 (diff) | |
Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.h')
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 94d02de9b..f9a711704 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -93,6 +93,8 @@ private: std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; //auxiliary variables std::vector< Node > d_aux_vars; + // relevant theory ids + std::vector< TheoryId > d_tids; //literals to equalities for aux vars std::map< Node, std::map< Node, Node > > d_aux_eq; //the CE variables |