diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-05 19:28:54 -0500 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-08-05 17:28:54 -0700 |
| commit | 57524fd9f204f8e85e5e37af1444a6f76d809aee (patch) | |
| tree | 9c8e4e0a90431921e0675397af1cdf106ad7a3a8 /proofs | |
| parent | d14fbb0eb27226e3a7d86733c087e469e797d1ef (diff) | |
Fix drat signature wrt side condition return types. (#3160)
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) |