Skip to content

Commit 718ec95

Browse files
committed
fix: reconstruction of uninterpreted sorts with >10 elements
1 parent 7d1d823 commit 718ec95

1 file changed

Lines changed: 4 additions & 1 deletion

File tree

Smt/Reconstruct/UF.lean

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,10 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
4646
let s := t.toString
4747
let endPos := (s.rawEndPos - t.getSort!.toString).decreaseBy 2
4848
let endPos := s.pos! (if endPos.dec.get? s == some '|' then endPos.dec else endPos)
49-
let startPos := (endPos.revFind? (· != '_')).get!
49+
let some sepPos := endPos.revFind? (· == '_') |
50+
throwError "failed to parse uninterpreted sort value index: {s}"
51+
let some startPos := sepPos.next? |
52+
throwError "failed to parse uninterpreted sort value index: {s}"
5053
let i : Nat := (s.extract startPos endPos).toNat!
5154
if h : i < n then
5255
let i : Fin n := ⟨i, h⟩

0 commit comments

Comments
 (0)