I found a situation where simply performing a solver.push(); solver.pop() pair (even with nothing between) causes a later call to solver.check to return unknown rather than sat. I was able to reduce the test case as far as:
Currently, this test returns unknown with the reason "(incomplete quantifiers)". However, without the "s.push(); s.pop()" on line 28, the call to s.check() returns sat (my actual code of course does more work between the push and pop, but
it wasn't necessary for the test case). This happens on both the master and unstable branches.