Non-prop squashes appear non-functional

[gebner]

#lang-pulse

ghost fn foo ()
  preserves pure (squash nat)
{
  ()
(*
- Failed to prove pure property: squash nat
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
*)
}