An unsuccessful attempt to verify a count down program using SBV.

SBVMostekCountdown.hs

import Control.Monad.IO.Class (liftIO)

import Data.SBV

import Data.SBV.Examples.BitPrecise.Legato

prover = z3 { verbose = True
            , redirectVerbose = Just "example.smt2"
            , timing = PrintTiming
            , printBase = 10
            }

------------------------------------------------------------------
-- * Counting down to zero
------------------------------------------------------------------

-- | This program expects a positive value in RegX register. It decrements
--   the value in the register until it becomes zero and then exits.
countdown :: Program
countdown = loop
    where loop = dex $
                 bne loop $
                 end

-- | Let us check a fundamental property of countdown program:
--   it must count down, transforming an arbitrary positive number into zero.
theoremCoundown :: IO ThmResult
theoremCoundown = proveWith prover thm
    where thm :: Symbolic SBool
          thm = do
              let mem = mkSFunArray (const 0)
              x <- sWord8 "x"
              constrain $ x .> 0
              -- The program has an expected behavior in case of a literal value
              -- x <- pure 4

              -- Initialize the register RegX with an arbitrary SWord8
              let machine = initMachine mem (x, 0, false, false)

              -- liftIO $ print machine
              -- Run the program and extract the final state of the machine
              let machine' = countdown machine

              -- liftIO $ print machine'
              -- Check if RegX contains zero
              pure $ getReg RegX machine' .== 0

Thanks to @LeventErkok I became aware of the notion of symbolic termination. The termination of the countdown program depends on a symbolic value.

Levek has kindly pointed me to a relevant SBV example symbolical GCD computation that should give an idea. Also, he recommended reading Section 7.4 of this paper.