From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 20 Dec 2021 14:03:29 +0000 (-0300)
Subject: [proofs] Fix helper LFSC script (#7845)
X-Git-Tag: cvc5-1.0.0~632
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a86b6177a0311d5de8ab1439890db84b290a66bd;p=cvc5.git

[proofs] Fix helper LFSC script (#7845)
---

diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 889455917..f4fe867c0 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -48,10 +48,10 @@ cp -r $SIG_DIR $BASE_DIR/share/lfsc
 cat << EOF > $BASE_DIR/bin/cvc5-lfsc-check.sh
 #!/bin/bash
 
-echo "=== Generate proof: \$@" 
+echo "=== Generate proof: \$@"
 $BASE_DIR/bin/cvc5-proof.sh \$@ > proof.plf
 
-echo "=== Check proof with LFSC" 
+echo "=== Check proof with LFSC"
 $BASE_DIR/bin/lfsc-check.sh proof.plf
 EOF
 chmod +x $BASE_DIR/bin/cvc5-lfsc-check.sh
@@ -77,7 +77,6 @@ SIG_DIR=$BASE_DIR/share/lfsc/signatures
 SIGS="\$SIG_DIR/core_defs.plf \\
     \$SIG_DIR/util_defs.plf \\
     \$SIG_DIR/theory_def.plf \\
-    \$SIG_DIR/type_checking_programs.plf \\
     \$SIG_DIR/nary_programs.plf \\
     \$SIG_DIR/boolean_programs.plf \\
     \$SIG_DIR/boolean_rules.plf \\