[SMT-LIB] UF unsat benchmarks without equality

Jean-Claude Royer Jean-Claude.Royer at mines-nantes.fr
Thu Mar 12 04:28:10 EDT 2015


Dear all,

I am looking for  unsatisfiable examples of first-order logic with uninterpreted functions
but without equality predicates.
There are benchmarks in UF but with equality.
Is there something elsewhere ?

regards


Jean-Claude.Royer at mines-nantes.fr
ASCOLA, Mines de Nantes - INRIA
+ 33 2 51 85 82 05








More information about the SMT-LIB mailing list