diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-11 09:17:06 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-11 09:17:06 -0500 |
| commit | 1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25 (patch) | |
| tree | d7d27d0938c3a1f2d5d9236e26d895c03adfd0d6 /src/theory/quantifiers/inst_propagator.h | |
| parent | 5e4ed407978b892e04de00994be535f58fb33257 (diff) | |
Minor fixes for inst match generators. Updates to qip.google
Diffstat (limited to 'src/theory/quantifiers/inst_propagator.h')
| -rw-r--r-- | src/theory/quantifiers/inst_propagator.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index a6f76ef44..0c02c7f95 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -72,7 +72,7 @@ private: std::map< Node, std::vector< Node > > d_uf_exp; Node getUfRepresentative( Node a, std::vector< Node >& exp ); /** disequality list, stores explanations */ - std::map< Node, std::map< Node, Node > > d_diseq_list; + std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list; /** add arg */ void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ); public: |