This tool generates a graphical representation of a model for a smt2 formula.
In case the supplied model does not restrict the formula to a single choice of variables, boolean expressions are shown as unknown (black/white). For bitvectors, values that together yield a model satisfying the expression are choosen.