diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 34920d08c..fd410ae14 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -119,7 +119,7 @@ jobs:
         set -e
         mkdir build
         cd build
-        CC=clang CXX=clang++ cmake -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -DBUILD_DOTNET_BINDINGS=True -G "Ninja" ../
+        CC=clang CXX=clang++ cmake -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -DBUILD_DOTNET_BINDINGS=False -G "Ninja" ../
         ninja
         ninja test-z3
         cd ..
diff --git a/src/model/model.cpp b/src/model/model.cpp
index b96fbccdb..f9998437d 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -527,6 +527,15 @@ bool model::is_true(expr_ref_vector const& ts) {
     return true;
 }
 
+bool model::is_false(expr_ref_vector const& ts) {
+    for (expr* t : ts) if (is_false(t)) return true;
+    return false;
+}
+
+bool model::are_equal(expr* s, expr* t) {
+    return m_mev.are_equal(s, t);
+}
+
 void model::reset_eval_cache() {
     m_mev.reset();
 }
diff --git a/src/model/model.h b/src/model/model.h
index a7a356be0..de31d08aa 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -94,6 +94,8 @@ public:
     bool is_true(expr* t);
     bool is_false(expr* t);
     bool is_true(expr_ref_vector const& ts);
+    bool is_false(expr_ref_vector const& ts);
+    bool are_equal(expr* s, expr* t);
     void reset_eval_cache();
     bool has_solver(); 
     void set_solver(expr_solver* solver);
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index ea89c6642..98df761c8 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -18,7 +18,6 @@ Notes:
 --*/
 #include "util/scoped_timer.h"
 #include "util/cancel_eh.h"
-#include "util/cooperate.h"
 #include "util/scoped_ptr_vector.h"
 #include "tactic/tactical.h"
 #include <thread>