From de1cf30ea85f6cef801504aa69951278726345f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Jul 2023 16:54:33 -0700 Subject: [PATCH] strengthen Tseitin checker to take true/false constants into account Signed-off-by: Nikolaj Bjorner --- src/sat/smt/tseitin_theory_checker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/tseitin_theory_checker.cpp b/src/sat/smt/tseitin_theory_checker.cpp index 74f4e55b0..ffddc9063 100644 --- a/src/sat/smt/tseitin_theory_checker.cpp +++ b/src/sat/smt/tseitin_theory_checker.cpp @@ -72,7 +72,7 @@ namespace tseitin { complement_mark(arg); for (expr* arg : *to_app(main_expr)) - if (!is_complement(arg)) + if (!is_complement(arg) && !m.is_true(arg)) return false; return true; @@ -178,7 +178,7 @@ namespace tseitin { for (expr* arg : *jst) mark(arg); for (expr* arg : *to_app(a)) - if (!is_marked(arg)) + if (!is_marked(arg) && !m.is_false(arg)) return false; return true; }