From 96ce991a4b8593f7ec831c3a9b40b214d2ac3761 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 14 Dec 2010 21:07:46 +0000
Subject: congruence closure module now supports things other than APPLY_UF;
 ported from "arrays" branch to trunk

---
 src/theory/uf/morgan/theory_uf_morgan.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory/uf')

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.
-- 
cgit v1.2.3