summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/get-lfsc-checker5
1 files changed, 2 insertions, 3 deletions
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 \\
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback