diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/signatures/drat.plf | 4 |
1 files 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) |