From c6b595d98140ef02bbf0a76a4af6b53813829cb3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Apr 2026 09:22:19 -0700 Subject: [PATCH] fix inverted logic of is-linear, #9311 Signed-off-by: Nikolaj Bjorner --- 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 36b61e9a2..2826e8ddd 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -321,7 +321,7 @@ namespace euf { if (!is_app(t)) return false; for (auto arg : *to_app(t)) - num_values += m.is_value(arg) ? 1 : 0; + num_values += m.is_value(arg) ? 0 : 1; return num_values <= 1; }