diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-12-14 21:07:46 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-12-14 21:07:46 +0000 |
| commit | 96ce991a4b8593f7ec831c3a9b40b214d2ac3761 (patch) | |
| tree | bf804dcc18a20394a6fba8ac4bed6932ca4c7c02 /src/theory/uf | |
| parent | b44f183a75deea11fa379554b893b6656e1864b2 (diff) | |
congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 99e6f5fbc..cbc5f1eab 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -74,7 +74,7 @@ private: /** * Instance of the congruence closure module. */ - CongruenceClosure<CongruenceChannel> d_cc; + CongruenceClosure<CongruenceChannel, CongruenceOperator<kind::APPLY_UF> > d_cc; /** * Our union find for equalities. |