diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index f99685854..2e8eab0e6 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -12,6 +12,7 @@ Author:
 --*/
 
 
+#include "ast/for_each_expr.h"
 #include "ast/simplifiers/model_reconstruction_trail.h"
 #include "ast/converters/generic_model_converter.h"
 
@@ -20,9 +21,9 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
     // accumulate a set of dependent exprs, updating m_trail to exclude loose 
     // substitutions that use variables from the dependent expressions.
     ast_mark free_vars;
-    auto [f, dep] = d;
+    auto [f, dep] = d();
     for (expr* t : subterms::all(expr_ref(f, m))) 
-        free_vars.mark(t);
+        free_vars.mark(t, true);
     
     NOT_IMPLEMENTED_YET();
 }
@@ -32,7 +33,7 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
  */
 model_converter_ref model_reconstruction_trail::get_model_converter() {
     model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
-    // walk the trail from the back.
+    // walk the trail from the back
     // add substitutions from the back to the generic model converter
     // after they have been normalized using a global replace that replaces 
     // substituted variables by their terms.
diff --git a/src/test/horn_subsume_model_converter.cpp b/src/test/horn_subsume_model_converter.cpp
index aea819d7a..95b14ea31 100644
--- a/src/test/horn_subsume_model_converter.cpp
+++ b/src/test/horn_subsume_model_converter.cpp
@@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
 --*/
 
 
-#include "tactic/horn_subsume_model_converter.h"
+#include "ast/converters/horn_subsume_model_converter.h"
 #include "ast/arith_decl_plugin.h"
 #include "model/model_smt2_pp.h"
 #include "ast/reg_decl_plugins.h"