From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 6 Aug 2019 00:28:54 +0000 (-0500)
Subject: Fix drat signature wrt side condition return types. (#3160)
X-Git-Tag: cvc5-1.0.0~4042
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57524fd9f204f8e85e5e37af1444a6f76d809aee;p=cvc5.git

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

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)