From 57524fd9f204f8e85e5e37af1444a6f76d809aee Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Aug 2019 19:28:54 -0500 Subject: [PATCH] Fix drat signature wrt side condition return types. (#3160) --- proofs/signatures/drat.plf | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index fa7ca3055..9f1ec00a9 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -325,7 +325,7 @@ ; Do unit propagation on `f`, constructing a UP model for it. -(program build_up_model ((f cnf)) clause +(program build_up_model ((f cnf)) UPConstructionResult (match (unit_search f) (USRBottom UPCRBottom) (USRNoUnit (UPCRModel cln)) @@ -338,7 +338,7 @@ ; Given some starting assignment (`up_model`), continue UP to construct a larger ; model. -(program extend_up_model ((f cnf) (up_model clause)) clause +(program extend_up_model ((f cnf) (up_model clause)) UPConstructionResult (do (clause_into_global up_model) (let result (build_up_model f) (do (clause_undo_into_global up_model) -- 2.30.2