From 266935bc6accb961f9112b1ce0087bcdfe2555ff Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 15 Jun 2023 11:08:38 +0200
Subject: [PATCH] [verification] Any invalid sub-formula results into invalid
formula.
---
src/verification.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/verification.ml b/src/verification.ml
index 3aa186a..707340b 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -178,6 +178,7 @@ let combine_prover_answers answers =
List.fold_left answers ~init:Call_provers.Valid ~f:(fun acc r ->
match (acc, r) with
| Call_provers.Valid, r | r, Call_provers.Valid -> r
+ | Invalid, _ | _, Invalid -> Invalid
| _ -> acc)
let answer_dataset limit config env prover config_prover driver dataset task =
--
GitLab