An uninterpreted constant was preregistered to the UF theory

[nafur]

This assertion seems to protect against users injecting uninterpreted constants from being put in constraints. The following input triggers this assertion, though without ever inspecting a model. Unfortunately it uses blockModelValues, thus it can't be converted to smtlib.

set-murxla-options -t 1 --cvc5 --reals --uf
90808 new
16668 set-option produce-models true
88701 set-option produce-unsat-assumptions true
32353 mk-sort SORT_REAL
      return s1
79794 mk-sort SORT_UNINTERPRETED _u0
      return s2
 1747 mk-sort SORT_BOOL
      return s3
56858 mk-sort SORT_UNINTERPRETED _u1
      return s4
19378 mk-sort SORT_UNINTERPRETED _u2
      return s5
79425 mk-const s5 "_x8"
      return t1
19950 mk-const s3 "_x10"
      return t2
36067 mk-const s4 "_x14"
      return t3
85330 mk-sort SORT_UNINTERPRETED _u15
      return s6
41292 mk-var s3 "_f24_0"
      return t4
41292 mk-var s6 "_f24_1"
      return t5
41292 mk-fun "_f24" 2 t4 t5 t4
      return t6 s7
16936 mk-var s1 "_f26_0"
      return t7
16936 mk-var s4 "_f26_1"
      return t8
16936 mk-var s4 "_f26_2"
      return t9
16936 mk-var s2 "_f26_3"
      return t10
16936 mk-var s4 "_f26_4"
      return t11
16936 mk-fun "_f26" 5 t7 t8 t9 t10 t11 t8
      return t12 s8
27889 check-sat-assuming 3 t2 t2 t2
57807 cvc5-block-model-values 4 t2 t6 t12 t3
89297 cvc5-simplify t1

terminate called after throwing an instance of 'cvc5::api::CVC5ApiException'
  what():  An uninterpreted constant was preregistered to the UF theory.

[ajreynol]

We need to disallow calling block-model-values on terms that involve uninterpreted sorts, I believe there is another issue for this.

[nafur]

Very similar to #420, possible a duplicate?

[ajreynol]

Yep, thats the one.