Bad error messages

[nikswamy]

1. Fails pointing to the equality and claiming that an SMT query failed

fn value_of (#a:Type) (r:ref a)
requires pts_to r 'v
returns v:a
ensures pts_to r 'v ** pure (v == 'v)
{
    'v
}

2. Points to the (!i) but fails saying expected int got stt int .... which is a bit cryptic

fn four_fail ()
requires emp
returns i:int
ensures pure (i == 4)
{
    let mut i = 1;
    add i (!i);
    add i (!i);
    !i
}

[nikswamy]

This program fails to check blaming the entire program, instead of just the equality of a == c * y.

fn multiply_by_repeated_addition (x y:nat)
    requires emp
    returns z:nat
    ensures pure (z == x * y)
{
    let mut ctr = 0;
    let mut acc : nat = 0;
    while (
        let c = !ctr;
        (c < x)
    )
    invariant b.
    exists* c a.
        pts_to ctr c **
        pts_to acc a **
        pure (//0 <= c /\
              c <= x /\
              a == (c * y) /\
              b == (c < x))
    {
        let a = !acc;
        acc := a + y;
        let c = !ctr;
        ctr := c + 1;
    };
    !acc
}

[gebner]

If you forget a pure on an assertion, Pulse says that it cannot prove the assertion (instead of complaining about the type error).

```pulse
fn foo (n: nat) requires pure (n >= 42) ensures emp {
  assert (n >= 1);
  // - Tactic logged issue:
  // - Cannot prove:
  //     op_GreaterThanOrEqual n 1
  // - In the context:
  //     emp
}