From aaabbfb594fcfed4240c580e31db51cc3483e6ed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Dec 2022 15:53:55 -0800 Subject: [PATCH] remove comment that does not align with result Signed-off-by: Nikolaj Bjorner --- src/tactic/core/nnf_tactic.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/core/nnf_tactic.h b/src/tactic/core/nnf_tactic.h index fa724f2b8..083380be8 100644 --- a/src/tactic/core/nnf_tactic.h +++ b/src/tactic/core/nnf_tactic.h @@ -47,7 +47,6 @@ Once all negations are pushed inside, the resulting formula is in NNF. (apply nnf) ``` -This would convert the formula (not (or (> x 0) (< x 0))) to (and (<= x 0) (>= x 0)), which is in NNF. ### Notes