Soundness bug in QF_UF

[numairmansur]

Hi,
On the following satisfiable formula, yices return unsat
38.smt2

$ ./yices_smt2 38.smt2
unsat

z3 and CVC4 return sat

Yices 2.6.2
Copyright SRI International.
Linked with GMP 6.1.2
Copyright Free Software Foundation, Inc.
Build date: 2020-02-12
Platform: x86_64-pc-linux-gnu (release)
Revision: 1526d93

[dddejan]

Thanks for the report.

In debug mode, we get assertion failure.

./yices_smt2 38.smt2 
Assertion failed: (n > 0 && sorted_array(c, n)), function constant_is_in_set, file context/symmetry_breaking.c, line 1170.

[BrunoDutertre]

This was a bug in the symmetry breaking code. It's fixed in b5f1d0a.