From e81dc5a0a00eede820eda0f8f9fa9876954b49b9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 26 Jun 2015 09:03:56 +0200
Subject: [PATCH] fixes issue #143 and memory leak on theory plugin setup

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/Context.cs  | 8 ++++----
 src/api/java/Context.java  | 8 ++++----
 src/api/java/FuncDecl.java | 2 +-
 src/smt/smt_context.cpp    | 4 +++-
 4 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index a717efbc2..eaf4e4777 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2238,7 +2238,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Check for set membership.
         /// </summary>
-        public Expr MkSetMembership(Expr elem, Expr set)
+        public BoolExpr MkSetMembership(Expr elem, Expr set)
         {
             Contract.Requires(elem != null);
             Contract.Requires(set != null);
@@ -2246,13 +2246,13 @@ namespace Microsoft.Z3
 
             CheckContextMatch(elem);
             CheckContextMatch(set);
-            return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
+            return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
         }
 
         /// <summary>
         /// Check for subsetness of sets.
         /// </summary>
-        public Expr MkSetSubset(Expr arg1, Expr arg2)
+        public BoolExpr MkSetSubset(Expr arg1, Expr arg2)
         {
             Contract.Requires(arg1 != null);
             Contract.Requires(arg2 != null);
@@ -2260,7 +2260,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(arg1);
             CheckContextMatch(arg2);
-            return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
+            return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
         }
         #endregion
 
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 1cab00342..b2d77e792 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1818,11 +1818,11 @@ public class Context extends IDisposable
     /**
      * Check for set membership.
      **/
-    public Expr mkSetMembership(Expr elem, Expr set)
+    public BoolExpr mkSetMembership(Expr elem, Expr set)
     {
         checkContextMatch(elem);
         checkContextMatch(set);
-        return Expr.create(
+        return (BoolExpr) Expr.create(
                 this,
                 Native.mkSetMember(nCtx(), elem.getNativeObject(),
                         set.getNativeObject()));
@@ -1831,11 +1831,11 @@ public class Context extends IDisposable
     /**
      * Check for subsetness of sets.
      **/
-    public Expr mkSetSubset(Expr arg1, Expr arg2)
+    public BoolExpr mkSetSubset(Expr arg1, Expr arg2)
     {
         checkContextMatch(arg1);
         checkContextMatch(arg2);
-        return Expr.create(
+        return (BoolExpr) Expr.create(
                 this,
                 Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
                         arg2.getNativeObject()));
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index f7e9de2b2..14f9bc9e7 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -50,7 +50,7 @@ public class FuncDecl extends AST
         FuncDecl casted = (FuncDecl) o;
         if (casted == null)
             return false;
-        return this == casted;
+        return this.getNativeObject() == casted.getNativeObject();
     }
 
     /**
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 36311af7e..6d39019c6 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2698,8 +2698,10 @@ namespace smt {
 #endif
 
     void context::register_plugin(theory * th) { 
-        if (m_theories.get_plugin(th->get_family_id()) != 0)
+        if (m_theories.get_plugin(th->get_family_id()) != 0) {
+            dealloc(th);
             return; // context already has a theory for the given family id.
+        }
         SASSERT(std::find(m_theory_set.begin(), m_theory_set.end(), th) == m_theory_set.end());
         SASSERT(!already_internalized_theory(th));
         th->init(this);