diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-12-20 11:03:29 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-20 08:03:29 -0600 |
| commit | a86b6177a0311d5de8ab1439890db84b290a66bd (patch) | |
| tree | 686fa14eed48652cc1e959a3b82b356d90bddcf4 | |
| parent | 99992303744ca89478aa077af71e6e5dd7885ee1 (diff) | |
[proofs] Fix helper LFSC script (#7845)
| -rwxr-xr-x | contrib/get-lfsc-checker | 5 |
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 \\ |