From 95e07ffe8e96ed18fda51f0ccdabfbe5f32d8b68 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 14 Nov 2022 19:14:51 -0800
Subject: [PATCH] disable unsound context equality solving
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/simplifiers/solve_eqs.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 0b6f12160..18928dca8 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -197,7 +197,7 @@ namespace euf {
if (!m.inc())
return;
- if (m_config.m_context_solve) {
+ if (m_config.m_context_solve && false) {
old_fmls.reset();
m_subst_ids.reset();
eqs.reset();