Generic solver fails SortingNetwork test

[makaimann]

This can be reproduced by changing https://github.com/makaimann/smt-switch/blob/3ba9442aef2def27faeb79185065ac1d481d26f7/tests/test-sorting-network.cpp#L104 to include generic solvers. Then configuring, building and running with:

./configure.sh --debug --cvc4
cd build
make
./tests/test-sorting-network

[makaimann]

@yoni206 would you be willing to look into this?

[makaimann]

Oh wait, @yoni206, I looked at it again and figured out the problem. It's because I build a term after calling check-sat. If I move this line https://github.com/makaimann/smt-switch/blob/3ba9442aef2def27faeb79185065ac1d481d26f7/tests/test-sorting-network.cpp#L79 before the call to check-sat, then it passes.

But I'm wondering if it has to be that way? Other solvers don't behave that way in the API at least.

[yoni206]

from page 52 of: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

In the generic solver, we use a define-fun for every make_term. According to this diagram, define-fun cannot be used right after check-sat when using the textual smtlib interface. Since other APIs don't fail for this, the generic solver should support this too. This can be fixed by, for example, calling define-fun lazily, only before assertions that use the created terms, but there could be other solutions.

[yoni206]

(from the same page)

I wasn't accurate -- it is ok to do a define-fun right after check-sat, but it moves you to Assert mode, in which you are not allowed to do get-value. BTW z3's smtlib interface does not complain.