Questionnaire-2024/smt_and_z3/0010.tex

\item \self Given a 4-bit bitvector $x$, we want to check whether it is possible that $x \cdot 2 > x \cdot 4 $.

The following python script returns \texttt{sat}. Explain the error in the script and expand it such that it correctly prints \texttt{unsat}.
\vskip7em

  \begin{pythonSourceCode}
      from z3 import *

      solver = Solver()

      bvX  = BitVec("bvX", 4)

      solver.add(UGT(bvX * 2,bvX * 4))




      result = solver.check()
      print(result)
      if result == sat:
          print(solver.model())
          print(solver.model().evaluate(bvX * 2))
          print(solver.model().evaluate(bvX * 4))
  \end{pythonSourceCode}
  \vskip3em