From 60967efd3803ddee4515ca7820da8e9e48af9386 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Sep 2022 18:39:21 -0700 Subject: [PATCH] fix wrong condition for delayed bit-blasting --- src/sat/smt/bv_delay_internalize.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index 6ad10c53aee..c3c457464f6 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -47,7 +47,7 @@ namespace bv { return true; unsigned num_vars = e->get_num_args(); for (expr* arg : *e) - if (!m.is_value(arg)) + if (m.is_value(arg)) --num_vars; if (num_vars <= 1) return true;