"FATAL ERROR: unexpected context status" when using (get-model) on an 'unknown' result

[GabrielVDSchot]

Hi there!

I'm currently trying out the timeout option (-t) for a SMT2 project. I'm sending in a bunch of assertions, with a call to (check-sat), and then to (get-model).

As expected, I get the right model when the result is 'sat', and an error when the result is 'unsat' since (get-model) is not supposed to be called in that case. However when a (check-sat) command times out, the result given by (check-sat) is 'unknown', and it seems yices2 does not known how to handle (get-model) in that case.

Here's what I'm getting :

unknown

*************************************************************
FATAL ERROR: BUG: unexpected context status
*************************************************************
Please report this bug to yices-bugs@csl.sri.com.
To help us diagnose this problem, please include the
following information in your bug report:

  Yices version: 2.6.2
  Build date: 2022-06-27
  Platform: x86_64-pc-linux-gnu (release)

Thank you for your help.
*************************************************************

BUG: unexpected context status

This is a problem, since according to the SMT-LIB documentation :

On reporting sat or unknown the solver should move to sat mode—and then respond to get-assignment, get-model, and get-value commands provided that the corresponding enabling option is set to true.

Here's a random sudoku.txt file which should easily time out and recreate the bug. Just launch :

yices-smt2 -t 3 sudoku.txt

sudoku.txt

[disteph]

Thanks for reporting. We fail with an error simply because we still don't have a model of the constraints. I'm not sure how to interpret this excerpt from the SMTLib doc, e.g. "move to sat mode". Does that involve resetting the set of constraints to the empty set and respond to the (get-model) query with any model? Or does the doc assume that the solver somehow had a putative and partial model when the timeout hit, and these next commands allow the user to inspect it, even if it's not a solution to the constraints? I'll try to understand what they meant when writing that.

[BrunoDutertre]

A workaround is to call yices with flag --incremental. That helps recover after timeouts. I'm also working on a fix that will replace the fatal error with there's not model. That should be a good enough approximation to the standard.