"Invalid query call" from repeated `query` under `runSMT`

[gergoerdi]

I am trying to run a symbolic (stateful) calculation with all-literal state and input, and then trying to get the output which should be concrete at this point. What I've tried:

module Main where

import Data.SBV
import Data.SBV.Control
import Control.Monad.State

foo :: State SInt16 SInt16
foo = do
    x <- get
    put $ x + 1
    return $ x * 2

main :: IO ()
main = do
    runSMT $ do
        s <- return $ literal 4

        (x, s) <- return $ flip runState s foo
        x <- query $ inNewAssertionStack $ do
             ensureSat
             getValue x
        liftIO $ print x

        (x, s) <- return $ flip runState s foo
        x <- query $ inNewAssertionStack $ do
             ensureSat
             getValue x
        liftIO $ print x

The first round works as expected, and prints 8. However, the second round fails with the following error message:

*** Data.SBV: Invalid query call.
***
***   Current mode: Satisfiability (User Query)
***
*** Query calls are only valid within runSMT/runSMTWith calls

I might be breaking some invariant with doing symbolic calculation after ensureSat, I don't know. Is this supposed to work?

However, at the very least the error message needs improvement because it is suggesting my problem is that I am not calling query under runSMT which I very much am.

[gergoerdi]

Just to show "what have I tried", I tried putting an inNewAssertionStack around the ensureSat >> getValue x but it doesn't seem to change anything.

[LeventErkok]

The error message is confusing indeed. I just pushed a fix, and now it says:

*** Exception:
*** Data.SBV: Invalid query call.
***
***   Current mode: Satisfiability (User Query)
***
*** Query calls are only valid within runSMT/runSMTWith calls,
*** and each call to runSMT should have only one query call inside.

which is a bit better I hope. Bottom line: There should be only one call to query. I'd code your program as follows:

main :: IO ()
main = do
    runSMT $ do
        s <- return $ literal 4

        (x, s) <- return $ flip runState s foo

        query $ do x <- inNewAssertionStack $ do
                          ensureSat
                          getValue x
                   liftIO $ print x

                   (x, s) <- return $ flip runState s foo

                   x <- inNewAssertionStack $ do
                          ensureSat
                          getValue x
                   liftIO $ print x

This produces:

*Main> main
8
10

[LeventErkok]

I'm closing this as it seems resolved. Please re-open if there are issues remaining.