fix: reconstruction of uninterpreted sorts with >10 elements

[dranov]

import Smt

set_option trace.smt.reconstruct.term true

example [Nonempty U]
    (u00 u01 u02 u03 u04 u05 u06 u07 u08 u09 u10 u11 u12 : U)
    (h00 : u00 ≠ u01 ∧ u00 ≠ u02 ∧ u00 ≠ u03 ∧ u00 ≠ u04 ∧ u00 ≠ u05 ∧
      u00 ≠ u06 ∧ u00 ≠ u07 ∧ u00 ≠ u08 ∧ u00 ≠ u09 ∧ u00 ≠ u10 ∧
      u00 ≠ u11 ∧ u00 ≠ u12)
    (h01 : u01 ≠ u02 ∧ u01 ≠ u03 ∧ u01 ≠ u04 ∧ u01 ≠ u05 ∧ u01 ≠ u06 ∧
      u01 ≠ u07 ∧ u01 ≠ u08 ∧ u01 ≠ u09 ∧ u01 ≠ u10 ∧ u01 ≠ u11 ∧
      u01 ≠ u12)
    (h02 : u02 ≠ u03 ∧ u02 ≠ u04 ∧ u02 ≠ u05 ∧ u02 ≠ u06 ∧ u02 ≠ u07 ∧
      u02 ≠ u08 ∧ u02 ≠ u09 ∧ u02 ≠ u10 ∧ u02 ≠ u11 ∧ u02 ≠ u12)
    (h03 : u03 ≠ u04 ∧ u03 ≠ u05 ∧ u03 ≠ u06 ∧ u03 ≠ u07 ∧ u03 ≠ u08 ∧
      u03 ≠ u09 ∧ u03 ≠ u10 ∧ u03 ≠ u11 ∧ u03 ≠ u12)
    (h04 : u04 ≠ u05 ∧ u04 ≠ u06 ∧ u04 ≠ u07 ∧ u04 ≠ u08 ∧ u04 ≠ u09 ∧
      u04 ≠ u10 ∧ u04 ≠ u11 ∧ u04 ≠ u12)
    (h05 : u05 ≠ u06 ∧ u05 ≠ u07 ∧ u05 ≠ u08 ∧ u05 ≠ u09 ∧ u05 ≠ u10 ∧
      u05 ≠ u11 ∧ u05 ≠ u12)
    (h06 : u06 ≠ u07 ∧ u06 ≠ u08 ∧ u06 ≠ u09 ∧ u06 ≠ u10 ∧ u06 ≠ u11 ∧
      u06 ≠ u12)
    (h07 : u07 ≠ u08 ∧ u07 ≠ u09 ∧ u07 ≠ u10 ∧ u07 ≠ u11 ∧ u07 ≠ u12)
    (h08 : u08 ≠ u09 ∧ u08 ≠ u10 ∧ u08 ≠ u11 ∧ u08 ≠ u12)
    (h09 : u09 ≠ u10 ∧ u09 ≠ u11 ∧ u09 ≠ u12)
    (h10 : u10 ≠ u11 ∧ u10 ≠ u12)
    (h11 : u11 ≠ u12) :
    False := by
  smt +model [h00, h01, h02, h03, h04, h05, h06, h07, h08, h09, h10, h11]

Before this change, this incorrectly reconstructed the model as:

unable to prove goal, either it is false or you need to provide more facts. Here is a potential counter-example:

  U = Fin 13
  u12 = 0
  u11 = 1
  u10 = 2 (note the repetition!!)
  u09 = 3
  u08 = 4
  u07 = 5
  u06 = 6
  u05 = 7
  u04 = 8
  u03 = 9
  u02 = 0
  u01 = 1
  u00 = 2 (!!)
[smt.reconstruct.term] u12 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u12 
[smt.reconstruct.term] u11 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u11 
[smt.reconstruct.term] u10 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u10 
[smt.reconstruct.term] u09 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u09 
[smt.reconstruct.term] u08 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u08 
[smt.reconstruct.term] u07 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u07 
[smt.reconstruct.term] u06 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u06 
[smt.reconstruct.term] u05 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u05 
[smt.reconstruct.term] u04 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u04 
[smt.reconstruct.term] u03 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u03 
[smt.reconstruct.term] u02 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u02 
[smt.reconstruct.term] u01 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u01 
[smt.reconstruct.term] u00 =(Smt.Reconstruct.Builtin.reconstructBuiltin)=> u00 
[smt.reconstruct.term] (as @U_0 U) =(Smt.Reconstruct.UF.reconstructUF)=> 0 
[smt.reconstruct.term] (as @U_1 U) =(Smt.Reconstruct.UF.reconstructUF)=> 1 
[smt.reconstruct.term] (as @U_2 U) =(Smt.Reconstruct.UF.reconstructUF)=> 2 
[smt.reconstruct.term] (as @U_3 U) =(Smt.Reconstruct.UF.reconstructUF)=> 3 
[smt.reconstruct.term] (as @U_4 U) =(Smt.Reconstruct.UF.reconstructUF)=> 4 
[smt.reconstruct.term] (as @U_5 U) =(Smt.Reconstruct.UF.reconstructUF)=> 5 
[smt.reconstruct.term] (as @U_6 U) =(Smt.Reconstruct.UF.reconstructUF)=> 6 
[smt.reconstruct.term] (as @U_7 U) =(Smt.Reconstruct.UF.reconstructUF)=> 7 
[smt.reconstruct.term] (as @U_8 U) =(Smt.Reconstruct.UF.reconstructUF)=> 8 
[smt.reconstruct.term] (as @U_9 U) =(Smt.Reconstruct.UF.reconstructUF)=> 9 
[smt.reconstruct.term] (as @U_10 U) =(Smt.Reconstruct.UF.reconstructUF)=> 0 
[smt.reconstruct.term] (as @U_11 U) =(Smt.Reconstruct.UF.reconstructUF)=> 1 
[smt.reconstruct.term] (as @U_12 U) =(Smt.Reconstruct.UF.reconstructUF)=> 2