mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

strengthen Tseitin checker to take true/false constants into account

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-28 16:54:33 -07:00
parent 6c5434f988
commit de1cf30ea8
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/tseitin_theory_checker.cpp
View file

@ -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;
}