Fatal failure CDHashMap::insertAtContextLevelZero() at src/context/cdhashmap.h:408

[mpreiner]

murxla/murxla@541e5f1
cvc5/cvc5@0f5ee6b

(set-option :global-declarations true)
(define-sort _s1 (_y2 _y2))

error:

Fatal failure within void cvc5::context::CDHashMap<Key, Data, HashFcn>::insertAtContextLevelZero(const Key&, const Data&) [with Key = std::__cxx11::basic_string<char>; Data = std::pair<std::vector<cvc5::api::Sort>, cvc5::api::Sort>; HashFcn = std::hash<std::__cxx11::basic_string<char> >] at cvc5/src/context/cdhashmap.h:408
Check failure

 d_map.find(k) == d_map.end()

Aborted (core dumped)

I know that the above is not valid SMT2 (minimized by ddsmt), but it should not trigger this assertion error in any case, but instead report a proper parse error. Error may be related to cvc5/cvc5#4767

[ajreynol]

I believe this is the same issue as cvc5/cvc5#4767.

[ajreynol]

Fixed by cvc5/cvc5@bcf90d5. Now gives this error:

(error "Parse Error: proj-issue407.smt2:2.27: Unexpected token: ')'.

  (define-sort _s1 (_y2 _y2))
                             ^
")