From 199d205a3d82376a39e0c4ad31160d80a8e04d3f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 27 Apr 2018 19:42:13 +0200
Subject: [PATCH] Fix #184.

---
 theories/heap_lang/lang.v  | 3 ++-
 theories/tests/heap_lang.v | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 39c6625fd..e4e5dc55a 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -351,10 +351,11 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   end.
 
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
+  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
   match v1, v2 with
   | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
   | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
-  | v1, v2 => guard (op = EqOp); Some $ LitV $ LitBool $ bool_decide (v1 = v2)
+  | _, _ => None
   end.
 
 Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 1e71aaba0..62b74b5e0 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -71,6 +71,11 @@ Section LiftingTests.
     wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
   Qed.
 
+  Definition heap_e6 : val := λ: "v", "v" = "v".
+
+  Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
+  Proof. wp_lam. wp_op. by case_bool_decide. Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in
-- 
GitLab