Fix drat signature wrt side condition return types. (#3160)

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index fa7ca305546bd68a3a527c0d2257b7e2698bb4f4..9f1ec00a9fb115207af29ea69e46a0267ecd9ffe 100644 (file)
--- 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)