From 02031377f430006a59f902814e3827077d379c55 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 17 Apr 2023 14:39:22 +0200
Subject: [PATCH] [vnnlib] Just simplify already negated formula.
---
src/printers/vnnlib.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml
index fe45152..29758ee 100644
--- a/src/printers/vnnlib.ml
+++ b/src/printers/vnnlib.ml
@@ -435,6 +435,7 @@ let print_goal info fmt (pr, t) =
let rec negate_term info t =
match t.Term.t_node with
+ | Tnot t -> t
| Tbinop (Tand, t1, t2) ->
Term.t_or (negate_term info t1) (negate_term info t2)
| Tbinop (Tor, t1, t2) ->
--
GitLab