diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 568ac79bf..e310f938c 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -429,11 +429,12 @@ namespace Microsoft.Z3
                 var lvl = BacktrackLevel;
                 BacktrackLevel = uint.MaxValue;
                 ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
-                if (r.Size == 1 && ((Expr)r[0]).IsFalse) {
+                var v = r.ToBoolExprArray();
+                if (v.Length == 1 && v[0].IsFalse) {
                    break;
                 }
-                yield return r.ToBoolExprArray();
-	        if (r.Size == 0) {
+                yield return v; 
+ 	            if (v.Length == 0) {
                    break;
                 }
 	     }
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index 629004869..7dec2f73b 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -87,5 +87,7 @@ void generic_model_converter::collect(ast_pp_util& visitor) {
 }
 
 void generic_model_converter::operator()(expr_ref& fml) {
+    // TODO: traverse expression and retrieve minimum trail index
+    // TODO: add func = expr starting at that index, removing from table if index is the same
     NOT_IMPLEMENTED_YET();
 }
diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h
index c58d0d029..1862efb8b 100644
--- a/src/tactic/generic_model_converter.h
+++ b/src/tactic/generic_model_converter.h
@@ -32,7 +32,9 @@ class generic_model_converter : public model_converter {
             m_f(f, m), m_def(d, m), m_instruction(i) {}
     };
     ast_manager& m;
-    vector<entry> m_entries;
+    vector<entry> m_add_entries;
+    vector<entry> m_hide_entries;
+    obj_map<func_decl_ref, unsigned> m_first_idx;
 public:
     generic_model_converter(ast_manager & m): m(m) {}
     
@@ -40,9 +42,9 @@ public:
     
     void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }
 
-    void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); }
+    void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); }
 
-    void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); }
+    void add(func_decl * d, expr* e) { m_add_entries.push_back(entry(d, e, m, ADD)); }
     
     virtual void operator()(model_ref & md, unsigned goal_idx);