From 0119d04899eac21a252465cdeace4eaf401422f9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 9 Aug 2017 20:54:53 +0200 Subject: [PATCH] Update after Dolmen change Dolmen Introduced a new 'Clause' statement, which has to be taken into account in the test executable of msat. --- src/main.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main.ml b/src/main.ml index 07381946..ecf0e38a 100644 --- a/src/main.ml +++ b/src/main.ml @@ -73,6 +73,10 @@ module Make match s.Dolmen.Statement.descr with | Dolmen.Statement.Def (id, t) -> T.def id t | Dolmen.Statement.Decl (id, t) -> T.decl id t + | Dolmen.Statement.Clause l -> + let cnf = T.antecedent (Dolmen.Term.or_ l) in + hyps := cnf @ !hyps; + S.assume cnf | Dolmen.Statement.Consequent t -> let cnf = T.consequent t in hyps := cnf @ !hyps;