jessie3: isqrt needs additional pre-condition

src/jessie/ACSLtoWhy3.ml

@@ -407,7 +407,12 @@ let rec term_node ~label t =
         match labels with
           | [] ->
             let ls = get_lsymbol li in
-            let args = List.map (fun x -> snd(term ~label x)) args in
+            let args = List.map (fun x -> 
+              let ty,t = term ~label x in
+              Self.result "arg = %a, type  = %a"
+              Cil_printer.pp_term x
+              Cil_printer.pp_logic_type ty;
+              t) args in
             t_app ls args
           | _ ->
             Self.not_yet_implemented "term_node Tapp with labels"

src/jessie/tests/demo/isqrt.c

@@ -6,6 +6,7 @@
 //@ logic integer sqr(integer x) = x * x;
 
 /*@ requires x >= 0;
+  @ requires x <= 1000000000; // not avoid integer overflow
   @ ensures \result >= 0 && sqr(\result+0) <= x && x < sqr(\result + 1);
   @*/
 int isqrt(int x) {