diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-16 09:29:15 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-16 09:29:15 +0100 |
| commit | 338ec2ee86e16423b265ba9bfc036606223f846f (patch) | |
| tree | 22f92c46fc4c70b839e74b13611c38f6277c3682 /src/theory/uf | |
| parent | 0042f301908763cf1edb8a2d56b3f373a0055908 (diff) | |
Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus parser.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 05fea6b5e..9cb2b5b53 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1539,7 +1539,8 @@ void StrongSolverTheoryUF::ensureEqcRec( Node n ) { /** has eqc */ bool StrongSolverTheoryUF::hasEqc( Node a ) { - return d_rel_eqc.find( a )!=d_rel_eqc.end() && d_rel_eqc[a]; + NodeBoolMap::iterator it = d_rel_eqc.find( a ); + return it!=d_rel_eqc.end() && (*it).second; } /** new node */ |