From 94b981024ed8a1b69a96a8eb7030c2164f1e5e16 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 1 Jun 2026 17:19:50 -0700
Subject: [PATCH] set up udoc relation to use datalog engine

---
 src/model/model_core.h     | 2 --
 src/test/udoc_relation.cpp | 3 ++-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/model/model_core.h b/src/model/model_core.h
index 6a52fa10b..8e531a2b6 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -72,8 +72,6 @@ public:
     void unregister_decl(func_decl * d);
     func_interp* update_func_interp(func_decl* f, func_interp* fi);
 
-    void add_lambda_defs();
-
     virtual expr * get_some_value(sort * s) = 0;
     virtual expr * get_fresh_value(sort * s) = 0;
     virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 9805f6169..57017f03c 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -6,6 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
 
 #include "muz/rel/udoc_relation.h"
 #include "util/trace.h"
+#include "util/gparams.h"
 #include "util/vector.h"
 #include "util/gparams.h"
 #include "ast/ast.h"
@@ -36,7 +37,7 @@ class udoc_tester {
 
     struct init {
         init(ast_manager& m) {
-            gparams::set("fp.engine", "datalog");
+            gparams::set("fp.engine", "datalog");                
             reg_decl_plugins(m);
         }
     };