fix smt that regressed with z3 bump to 4.12.2

all else being equal, works with 4.12.1, fails with 4.12.2 fails with all other solvers
EasyCrypt · Aug 7, 2023 · 900ba4c · 900ba4c
1 parent c7e7234
commit 900ba4c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/distributions/DBool.ec b/theories/distributions/DBool.ec
@@ -82,7 +82,7 @@ lemma dmap_pred (d: 'a distr) (p: 'a -> bool) :
 proof.
 move => d_ll; apply eq_distr => x.
 rewrite dbiased1E clamp_id; first by smt(ge0_mu le1_mu).
-rewrite dmap1E /(\o) /pred1; smt(mu_not).
+by rewrite dmap1E /(\o) /pred1 -d_ll -mu_not /#.
 qed.
 
 lemma dbiased1 : dbiased 1%r = dunit true.