projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 47eb5ed)
Minor sync from proof-new (#8293)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 13 Mar 2022 01:31:56 +0000 (19:31 -0600)
committerGitHub <noreply@github.com>
Sun, 13 Mar 2022 01:31:56 +0000 (01:31 +0000)
proofs/lfsc/signatures/boolean_rules.plf patch | blob | history

diff --git a/proofs/lfsc/signatures/boolean_rules.plf b/proofs/lfsc/signatures/boolean_rules.plf
index af16af1f9e431a5a477bfc4ef5313d8d1b3cb5cb..05a6347ec7ea0e7223a13d141992625c25e7cc7b 100644 (file)
--- a/proofs/lfsc/signatures/boolean_rules.plf
+++ b/proofs/lfsc/signatures/boolean_rules.plf
@@ -49,4 +49,4 @@
 
 ; Process scope, which is used to translate PfRule::SCOPE. It runs the side
 ; condition sc_process_scope on f to generate an equivalent formula g.
-(declare process_scope (! f term (! g term (! c term (! p1 (holds f) (! r (^ (sc_process_scope f c) g) (holds g))))))
+(declare process_scope (! f term (! g term (! c term (! p1 (holds f) (! r (^ (sc_process_scope f c) g) (holds g)))))))