From bfe4673daccdff1b48bfd59d5c5c674a83dab178 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Jan 2025 16:23:18 -0800 Subject: [PATCH] this check is not an invariant in the first place but nice to have. --- src/ast/sls/sls_arith_clausal.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp index 45ef15470..f42796419 100644 --- a/src/ast/sls/sls_arith_clausal.cpp +++ b/src/ast/sls/sls_arith_clausal.cpp @@ -281,7 +281,7 @@ namespace sls { tout << mk_bounded_pp(ctx.atom(bv), a.m) << "\n"; ctx.display(tout);); } - VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv)); + // VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv)); }); }