Bug in model construction from API, in Yices/CDCL(T)

[disteph]

Minimal counter-example:

(set-logic all)
(declare-sort p 0)
(declare-fun s () p)
(declare-fun p (p) p)
(assert (and (= (p s) (_ Const 1 p)) (= (_ Const 2 p) (p (_ Const 0 p)))))
(check-sat)
(get-model)

(_ Const 1 p) is obviously not SMTLib2 syntax. The above is simply reflecting a series of API calls, where (_ Const 1 p) denotes the constant 1 of the uninterpreted type p, as given by the API call to term_t yices_constant(type_t tau, int32_t i).

I've got a parser for this extended SMTLib2 syntax, if needed.

[disteph]

Assertion ailure is:

Assertion failed: (d[j].function != f || !mappings_match(table, i, d[j].map)), function add_hash_pair, file concrete_values.c, line 265.