From fdc042aee34e41ab420a96bdc36234799757979a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 26 Jan 2019 12:51:58 -0600 Subject: [PATCH] fix: no need to add trivial clauses at all --- src/core/Internal.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 9c18bdbd..0e27a550 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1500,7 +1500,6 @@ module Make(Plugin : PLUGIN) ) ) with Trivial -> - Vec.push vec init; Log.debugf info (fun k->k "Trivial clause ignored : @[%a@]" Clause.debug init) let[@inline never] flush_clauses_ st =