Skip to content

Commit

Permalink
HolSmt: parse assign-bounds index in arith rules
Browse files Browse the repository at this point in the history
This commit fixes a parsing error when parsing arithmetic `th-lemma`
inference rules with an `assign-bounds` parameter, i.e.:

((_ th-lemma arith assign-bounds ...) ...)

The error was due to `assign-bounds` not being in the known term
dictionary.
  • Loading branch information
someplaceguy authored and mn200 committed Apr 9, 2024
1 parent aee048a commit 70bec8c
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/HolSmt/Z3_ProofParser.sml
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,8 @@ local
("and-elim", one_prem "and-elim"),
(* the following is used in `(_ th-lemma arith ...)` inference rules *)
("arith", builtin_name "arith"),
(* the following is used in `(_ th-lemma arith ...)` inference rules *)
("assign-bounds", builtin_name "assign-bounds"),
(* the following is used in `(_ th-lemma bv ...)` inference rules *)
("bv", builtin_name "bv"),
("asserted", zero_prems "asserted"),
Expand Down

0 comments on commit 70bec8c

Please sign in to comment.