diff --git a/dune-project b/dune-project
index 6f9f1e3f3..4157f5b89 100644
--- a/dune-project
+++ b/dune-project
@@ -22,7 +22,7 @@
   dune-site
   markdown
   (pcre2 (>= 8))
-  (why3 (and (>= 1.8.0) (< 1.9)))
+  (why3 (and (>= 1.9.0) (< 1.10)))
   yojson
   (zarith (>= 1.10))
 ))
diff --git a/easycrypt.opam b/easycrypt.opam
index b74bc6fe4..25bfa8f46 100644
--- a/easycrypt.opam
+++ b/easycrypt.opam
@@ -10,7 +10,7 @@ depends: [
   "dune-site"
   "markdown"
   "pcre2" {>= "8"}
-  "why3" {>= "1.8.0" & < "1.9"}
+  "why3" {>= "1.9.0" & < "1.10"}
   "yojson"
   "zarith" {>= "1.10"}
   "odoc" {with-doc}
diff --git a/flake.lock b/flake.lock
index fc0e38f60..4185730b5 100644
--- a/flake.lock
+++ b/flake.lock
@@ -21,11 +21,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1731533236,
-        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "lastModified": 1791914995,
+        "narHash": "sha256-Zf/xfQEAasnwnmEfHqW/4hjDE/s44yn2hD4RuVIZRjA=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "rev": "b7a79d3fea1e214f6d668d521cecec0c01e26544",
         "type": "github"
       },
       "original": {
@@ -142,15 +142,17 @@
         "nixpkgs-python38": "nixpkgs-python38",
         "nixpkgs-python39": "nixpkgs-python39",
         "opam-overlays": "opam-overlays",
-        "opam-repository": "opam-repository",
+        "opam-repository": [
+          "opam-repository"
+        ],
         "opam2json": "opam2json"
       },
       "locked": {
-        "lastModified": 1782476416,
-        "narHash": "sha256-oFdLuHny6fe6kSOrOTN5Bfls+GisFiM8ytYrBQpGRog=",
+        "lastModified": 1789633723,
+        "narHash": "sha256-QfbCEvTKWnyMICHDA4rpq/GxtfhMNIlddUpF3Y85FIc=",
         "owner": "tweag",
         "repo": "opam-nix",
-        "rev": "583fb2ed4db44fcda4f6222c554949503d50a352",
+        "rev": "c6a5487ee20d976bb4eb08c0c92a693178206eb4",
         "type": "github"
       },
       "original": {
@@ -178,16 +180,17 @@
     "opam-repository": {
       "flake": false,
       "locked": {
-        "lastModified": 1784065055,
-        "narHash": "sha256-yT+DNlquArnWu8ZQ1uVEKE/HUuo7ZNwyOT8yvqiL30c=",
+        "lastModified": 1793156192,
+        "narHash": "sha256-JdL3wCFRcyWhcp8Yf2Csn0pq3g9t47Y20R0zzWo+HCA=",
         "owner": "ocaml",
         "repo": "opam-repository",
-        "rev": "8b272f4f03d431daf02557fa2c4b788825c6aae2",
+        "rev": "d84cf31c7dc731a040a072ad455a629ac0909e30",
         "type": "github"
       },
       "original": {
         "owner": "ocaml",
         "repo": "opam-repository",
+        "rev": "d84cf31c7dc731a040a072ad455a629ac0909e30",
         "type": "github"
       }
     },
@@ -221,21 +224,22 @@
           "nixpkgs"
         ],
         "opam-nix": "opam-nix",
+        "opam-repository": "opam-repository",
         "stable": "stable"
       }
     },
     "stable": {
       "locked": {
-        "lastModified": 1717179513,
-        "narHash": "sha256-vboIEwIQojofItm2xGCdZCzW96U85l9nDW3ifMuAIdM=",
+        "lastModified": 1780145889,
+        "narHash": "sha256-md0zn0RnwNvPyASas1yG5YUuwQ4ALA6ucL50l0DvqCo=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "63dacb46bf939521bdc93981b4cbb7ecb58427a0",
+        "rev": "8c50a710ddca43d7a530fb805ad55bde8d0141c5",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "24.05",
+        "ref": "26.05",
         "repo": "nixpkgs",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 66285c9c1..bed373d66 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,12 +1,17 @@
 {
   inputs = {
     opam-nix.url = "github:tweag/opam-nix";
+    opam-nix.inputs.opam-repository.follows = "opam-repository";
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable.url = "github:nixos/nixpkgs/24.05";
+    stable.url = "github:nixos/nixpkgs/26.05";
     nixpkgs.follows = "opam-nix/nixpkgs";
 
+    opam-repository = {
+      url = "github:ocaml/opam-repository/d84cf31c7dc731a040a072ad455a629ac0909e30";
+      flake = false;
+    };
   };
 
   outputs = { self, flake-utils, opam-nix, nixpkgs, ... }@inputs:
diff --git a/src/ecSmt.ml b/src/ecSmt.ml
index f51a52a5b..e3937a63c 100644
--- a/src/ecSmt.ml
+++ b/src/ecSmt.ml
@@ -705,10 +705,13 @@ and trans_form ((genv, lenv) as env : tenv * lenv) (fp : form) =
   | Flocal _ -> trans_app env fp []
   | Fop    _ -> trans_app env fp []
 
-    (* Special case for `%r` *)
+    (* Special case for `%r`. An integer literal is never negative
+       ([f_int] builds the opposite of a non-negative literal), and
+       why3 real constants carry their sign apart from the mantissa. *)
   | Fapp({ f_node = Fop (p, [])},  [{f_node = Fint n}])
       when p_equal p CI_Real.p_real_of_int ->
-    WTerm.t_real_const (BI.to_why3 n)
+    assert (0 <= BI.sign n);
+    WTerm.t_real_const ~is_neg:false (BI.to_why3 n)
 
   | Fapp (f,args) -> trans_app env f (List.map (trans_form env) args)