unsound result with MCSAT

[numairmansur]

Hi,
For the following file, yices returns an unsound result with mcsat. The
example is from the theory QF_UFLRA and is satisfiable.

856.smt2.zip

Without mcsat, yices returns the correct answer. Both CVC4 and z3 returns "sat"

OS:
NAME="Ubuntu"
VERSION="16.04.1 LTS (Xenial Xerus)"
ID=ubuntu
ID_LIKE=debian
PRETTY_NAME="Ubuntu 16.04.1 LTS"
VERSION_ID="16.04"

$ git log -1
commit 98fa2d8
Author: Bruno Dutertre bruno@csl.sri.com
Date: Mon Dec 2 22:19:33 2019 -0800
One more regression test

[dddejan]

In debug mode this returns

$ ./yices_smt2 --mcsat --incremental 856.smt2 
sat
sat
sat
sat
sat
sat
sat
Assertion failed: (rep_var != variable_null), function uf_plugin_propagate_apps, file mcsat/uf/uf_plugin.c, line 623.

[dddejan]

Note: reimplementation of QF_UF in the mcsat-bv branch does not fail.