From 5a8154c1564908ef4be5c98fcc973bfba36e9dd3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 Feb 2018 14:47:16 -0800
Subject: [PATCH] fix errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/solver/solver_na2as.cpp | 4 ++--
src/solver/solver_na2as.h | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index ae4014c7f..3cffd40cf 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -32,7 +32,7 @@ solver_na2as::~solver_na2as() {}
void solver_na2as::assert_expr_core(expr * t, expr * a) {
if (a == 0) {
- assert_expr_core(t);
+ solver::assert_expr_core(t);
}
else {
SASSERT(is_uninterp_const(a));
@@ -41,7 +41,7 @@ void solver_na2as::assert_expr_core(expr * t, expr * a) {
m_assumptions.push_back(a);
expr_ref new_t(m);
new_t = m.mk_implies(a, t);
- assert_expr_core(new_t);
+ solver::assert_expr_core(new_t);
}
}
diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h
index 061d62aee..2cbaaba5a 100644
--- a/src/solver/solver_na2as.h
+++ b/src/solver/solver_na2as.h
@@ -35,7 +35,7 @@ public:
virtual ~solver_na2as();
void assert_expr_core(expr * t, expr * a) override;
- virtual void assert_expr_core(expr * t) = 0;
+ // virtual void assert_expr_core(expr * t) = 0;
// Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);