diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index 5c722c828..25b3136ad 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -86,6 +86,8 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     Log.cs
     Model.cs
     NativeContext.cs
+    NativeFuncInterp.cs
+    NativeModel.cs
     Optimize.cs
     ParamDescrs.cs
     Params.cs
diff --git a/src/api/dotnet/NativeFuncInterp.cs b/src/api/dotnet/NativeFuncInterp.cs
new file mode 100644
index 000000000..718462af9
--- /dev/null
+++ b/src/api/dotnet/NativeFuncInterp.cs
@@ -0,0 +1,225 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    NativeFuncInterp.cs
+
+Abstract:
+
+    Z3 Managed API: Function Interpretations
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-21
+
+Notes:
+    
+--*/
+
+using System.Diagnostics;
+using System;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    ///  A function interpretation is represented as a finite map and an 'else' value.
+    ///  Each entry in the finite map represents the value of a function given a set of arguments.  
+    /// </summary>
+    public class NativeFuncInterp : IDisposable
+    {
+
+#if false
+        /// <summary>
+        /// An Entry object represents an element in the finite map used to encode
+        /// a function interpretation.
+        /// </summary>
+        public class Entry : Z3Object
+        {
+            /// <summary>
+            /// Return the (symbolic) value of this entry.
+            /// </summary>
+            public Expr Value
+            {
+                get
+                {
+                    return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
+                }
+            }
+
+            /// <summary>
+            /// The number of arguments of the entry.
+            /// </summary>
+            public uint NumArgs
+            {
+                get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
+            }
+
+            /// <summary>
+            /// The arguments of the function entry.
+            /// </summary>
+            public Expr[] Args
+            {
+                get
+                {
+
+                    uint n = NumArgs;
+                    Expr[] res = new Expr[n];
+                    for (uint i = 0; i < n; i++)
+                        res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
+                    return res;
+                }
+            }
+
+            /// <summary>
+            /// A string representation of the function entry.
+            /// </summary>
+            public override string ToString()
+            {
+                uint n = NumArgs;
+                string res = "[";
+                Expr[] args = Args;
+                for (uint i = 0; i < n; i++)
+                    res += args[i] + ", ";
+                return res + Value + "]";
+            }
+
+            #region Internal
+            internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
+
+            internal class DecRefQueue : IDecRefQueue
+            {
+                public DecRefQueue() : base() { }
+                public DecRefQueue(uint move_limit) : base(move_limit) { }
+                internal override void IncRef(Context ctx, IntPtr obj)
+                {
+                    Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
+                }
+
+                internal override void DecRef(Context ctx, IntPtr obj)
+                {
+                    Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
+                }
+            };
+
+            internal override void IncRef(IntPtr o)
+            {
+                Context.FuncEntry_DRQ.IncAndClear(Context, o);
+                base.IncRef(o);
+            }
+
+            internal override void DecRef(IntPtr o)
+            {
+                Context.FuncEntry_DRQ.Add(o);
+                base.DecRef(o);
+            }
+            #endregion
+        };
+
+        /// <summary>
+        /// The number of entries in the function interpretation.
+        /// </summary>
+        public uint NumEntries
+        {
+            get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
+        }
+
+        /// <summary>
+        /// The entries in the function interpretation
+        /// </summary>
+        public Entry[] Entries
+        {
+            get
+            {
+
+                uint n = NumEntries;
+                Entry[] res = new Entry[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// The (symbolic) `else' value of the function interpretation.
+        /// </summary>
+        public Expr Else
+        {
+            get
+            {
+
+                return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// The arity of the function interpretation
+        /// </summary>
+        public uint Arity
+        {
+            get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
+        }
+
+        /// <summary>
+        /// A string representation of the function interpretation.
+        /// </summary>    
+        public override string ToString()
+        {
+            string res = "";
+            res += "[";
+            foreach (Entry e in Entries)
+            {
+                uint n = e.NumArgs;
+                if (n > 1) res += "[";
+                Expr[] args = e.Args;
+                for (uint i = 0; i < n; i++)
+                {
+                    if (i != 0) res += ", ";
+                    res += args[i];
+                }
+                if (n > 1) res += "]";
+                res += " -> " + e.Value + ", ";
+            }
+            res += "else -> " + Else;
+            res += "]";
+            return res;
+        }
+
+#endif
+
+        #region Internal
+	NativeContext Context;
+	IntPtr NativeObject;
+	internal NativeFuncInterp(NativeContext ctx, IntPtr obj)
+        {
+	    Context = ctx;
+	    NativeObject = obj;
+            Debug.Assert(ctx != null);
+	    // inc-ref
+        }
+
+        /// <summary>
+        /// Finalizer.
+        /// </summary>
+        ~NativeFuncInterp()
+	{
+	     Dispose();
+	}
+
+        /// <summary>
+        /// Disposes of the underlying native Z3 object.
+        /// </summary>
+        public void Dispose()
+        {
+            if (NativeObject != IntPtr.Zero)
+            {
+	    	Native.Z3_func_interp_dec_ref(Context.nCtx, NativeObject);
+                NativeObject = IntPtr.Zero;                
+            }
+            GC.SuppressFinalize(this);
+        }
+
+
+        #endregion
+    }
+}
diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs
new file mode 100644
index 000000000..8a31af32f
--- /dev/null
+++ b/src/api/dotnet/NativeModel.cs
@@ -0,0 +1,329 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    NativeModel.cs
+
+Abstract:
+
+    Z3 Managed API: Models
+    Native interface to model objects.    
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-21
+    Nikolaj Bjorner (nbjorner) 2022-03-01
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics;
+using System.Collections.Generic;
+
+namespace Microsoft.Z3
+{
+    using Z3_context = System.IntPtr;
+    using Z3_ast = System.IntPtr;
+    using Z3_app = System.IntPtr;
+    using Z3_sort = System.IntPtr;
+    using Z3_func_decl = System.IntPtr;
+    using Z3_model = System.IntPtr;
+    using Z3_func_interp = System.IntPtr;
+    using Z3_func_entry = System.IntPtr;
+
+    /// <summary>
+    /// A Model contains interpretations (assignments) of constants and functions. 
+    /// </summary>
+    public class NativeModel
+    {
+        /// <summary>
+        /// Retrieves the interpretation (the assignment) of <paramref name="a"/> in the model. 
+        /// </summary>
+        /// <param name="a">A Constant</param>
+        /// <returns>An expression if the constant has an interpretation in the model, null otherwise.</returns>
+        public Z3_ast ConstInterp(Z3_ast a) => ConstInterp(Native.Z3_get_app_decl(Context.nCtx, a));
+
+        /// <summary>
+        /// Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model. 
+        /// </summary>
+        /// <param name="f">A function declaration of zero arity</param>
+        /// <returns>An expression if the function has an interpretation in the model, null otherwise.</returns>    
+        public Z3_ast ConstFuncInterp(Z3_func_decl f)
+        {
+            if (Native.Z3_get_arity(Context.nCtx, f) != 0) 
+                throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
+
+            return Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
+        }
+
+        /// <summary>
+        /// Retrieves the interpretation (the assignment) of a non-constant <paramref name="f"/> in the model. 
+        /// </summary>
+        /// <param name="f">A function declaration of non-zero arity</param>
+        /// <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns> 
+        public NativeFuncInterp FuncInterp(Z3_func_decl f)
+        {
+
+            Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f));
+	    
+            if (Native.Z3_get_arity(Context.nCtx, f) == 0) 
+            {
+                IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
+
+                if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
+                {
+                    if (n == IntPtr.Zero)
+                        return null;
+                    else
+                    {
+                        if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
+                            throw new Z3Exception("Argument was not an array constant");
+                        var fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
+                        return new NativeFuncInterp(Context, fd);
+                    }
+                }
+                else
+                {
+                    throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
+                }
+            }
+            else
+            {
+                IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f);
+                if (n == IntPtr.Zero)
+                    return null;
+                else
+                    return new NativeFuncInterp(Context, n);
+            }
+        }
+
+
+
+        /// <summary>
+        /// The number of constants that have an interpretation in the model.
+        /// </summary>
+        public uint NumConsts
+        {
+            get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
+        }
+
+
+        /// <summary>
+        /// The function declarations of the constants in the model.
+        /// </summary>
+        public Z3_func_decl[] ConstDecls
+        {
+            get
+            {
+
+                uint n = NumConsts;
+                Z3_func_decl[] res = new Z3_func_decl[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
+                return res;
+            }
+        }
+
+
+        /// <summary>
+        /// Enumerate constants in model.
+        /// </summary>
+        public IEnumerable<KeyValuePair<Z3_func_decl, Z3_ast>> Consts
+        {
+            get
+            {
+                uint nc = NumConsts;
+                for (uint i = 0; i < nc; ++i)
+                {
+                    var f = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
+                    IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
+                    if (n == IntPtr.Zero) continue;
+                    yield return new KeyValuePair<Z3_func_decl, Z3_ast>(f, n);
+                }
+            }
+        }
+
+
+        /// <summary>
+        /// The number of function interpretations in the model.
+        /// </summary>
+        public uint NumFuncs
+        {
+            get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
+        }
+
+#if false
+
+        /// <summary>
+        /// The function declarations of the function interpretations in the model.
+        /// </summary>
+        public FuncDecl[] FuncDecls
+        {
+            get
+            {
+
+                uint n = NumFuncs;
+                FuncDecl[] res = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// All symbols that have an interpretation in the model.
+        /// </summary>
+        public FuncDecl[] Decls
+        {
+            get
+            {
+
+                uint nFuncs = NumFuncs;
+                uint nConsts = NumConsts;
+                uint n = nFuncs + nConsts;
+                FuncDecl[] res = new FuncDecl[n];
+                for (uint i = 0; i < nConsts; i++)
+                    res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
+                for (uint i = 0; i < nFuncs; i++)
+                    res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));                
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
+        /// </summary>
+        public class ModelEvaluationFailedException : Z3Exception
+        {
+            /// <summary>
+            /// An exception that is thrown when model evaluation fails.
+            /// </summary>
+            public ModelEvaluationFailedException() : base() { }
+        }
+
+        /// <summary>
+        /// Evaluates the expression <paramref name="t"/> in the current model.
+        /// </summary>
+        /// <remarks>
+        /// This function may fail if <paramref name="t"/> contains quantifiers, 
+        /// is partial (MODEL_PARTIAL enabled), or if <paramref name="t"/> is not well-sorted.
+        /// In this case a <c>ModelEvaluationFailedException</c> is thrown.
+        /// </remarks>
+        /// <param name="t">An expression</param>
+        /// <param name="completion">
+        /// When this flag is enabled, a model value will be assigned to any constant 
+        /// or function that does not have an interpretation in the model.
+        /// </param>
+        /// <returns>The evaluation of <paramref name="t"/> in the model.</returns>        
+        public Z3_ast Eval(Z3_ast t, bool completion = false)
+        {
+            Debug.Assert(t != null);
+
+            IntPtr v = IntPtr.Zero;
+            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0)
+                throw new ModelEvaluationFailedException();
+            else
+                return Z3_ast.Create(Context, v);
+        }
+
+        /// <summary>
+        /// Alias for <c>Eval</c>.
+        /// </summary>        
+        public Z3_ast Evaluate(Z3_ast t, bool completion = false)
+        {
+            Debug.Assert(t != null);
+
+            return Eval(t, completion);
+        }
+
+        /// <summary>
+        /// Evaluate expression to a double, assuming it is a numeral already.
+        /// </summary>
+        public double Double(Z3_ast t) {
+            var r = Eval(t, true);
+            return Native.Z3_get_numeral_double(Context.nCtx, r);	    
+        }
+
+        /// <summary>
+        /// The number of uninterpreted sorts that the model has an interpretation for.
+        /// </summary>    
+        public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }
+
+        /// <summary>
+        /// The uninterpreted sorts that the model has an interpretation for. 
+        /// </summary>
+        /// <remarks>
+        /// Z3 also provides an interpretation for uninterpreted sorts used in a formula.
+        /// The interpretation for a sort is a finite set of distinct values. We say this finite set is
+        /// the "universe" of the sort.
+        /// </remarks>
+        /// <seealso cref="NumSorts"/>
+        /// <seealso cref="SortUniverse"/>
+        public Sort[] Sorts
+        {
+            get
+            {
+
+                uint n = NumSorts;
+                Sort[] res = new Sort[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+#endif
+
+        /// <summary>
+        /// Conversion of models to strings. 
+        /// </summary>
+        /// <returns>A string representation of the model.</returns>
+        public override string ToString()
+        {
+            return Native.Z3_model_to_string(Context.nCtx, NativeObject);
+        }
+
+
+
+	IntPtr NativeObject;
+	NativeContext Context;
+	
+        internal NativeModel(NativeContext ctx, IntPtr obj)
+        {
+	    Context = ctx;
+	    NativeObject = obj;
+            Debug.Assert(ctx != null);
+	    Native.Z3_model_inc_ref(ctx.nCtx, obj);
+        }
+
+
+        /// <summary>
+        /// Finalizer.
+        /// </summary>
+        ~NativeModel()
+	{
+	     Dispose();
+	}
+
+        /// <summary>
+        /// Disposes of the underlying native Z3 object.
+        /// </summary>
+        public void Dispose()
+        {
+            if (NativeObject != IntPtr.Zero)
+            {
+	    	Native.Z3_model_dec_ref(Context.nCtx, NativeObject);
+                NativeObject = IntPtr.Zero;                
+            }
+            GC.SuppressFinalize(this);
+        }
+
+
+    }
+}
+
+
+