Commit b9dd9456 authored by Heiko Becker's avatar Heiko Becker

Add a check for equality of values in environment

parent 0fda669f
......@@ -115,7 +115,13 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
&& validErrorbound e2 typeMap A (NatSet.add x dVars)
then
match FloverMap.find e1 A, FloverMap.find (Var Q x) A with
| Some (iv_e, err_e), Some (iv_x, err_x) => Qeq_bool err_e err_x
| Some (iv_e, err_e), Some (iv_x, err_x) =>
if (Qeq_bool err_e err_x)
then
match FloverMap.find e2 A with
| Some (iv_e2, err_e2) => Qeq_bool err_e2 err
| _,_ => false
else false
| _,_ => false
end
else false
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment