diff --git a/checkerScript.sml b/checkerScript.sml
index 67ed56954f74dbcea46d97b5c4cc0758100ee7ab..ae665fa6a1500f7141a185ddcd65ca9075aeed2d 100644
--- a/checkerScript.sml
+++ b/checkerScript.sml
@@ -79,7 +79,7 @@ Definition validateZerosLeqErr_def:
     in
       if ~ (validBounds iv realZeros ∧ recordered (FST iv) realZeros (SND iv)) then
           (Invalid "Zeros not correctly spaced", 0)
-      else if ~ (LENGTH realZeros = numZeros) then
+      else if LENGTH realZeros < numZeros then
           (Invalid "Did not find sufficient zeros", 0)
       else if globalErr ≤ eps
       then (Valid, globalErr)
diff --git a/realZeroLib.sml b/realZeroLib.sml
index 1fda9a4afe4d2eed8b53820c3fb201079fb18fc5..b885be2e119051983f77a40d410051fc18438303 100644
--- a/realZeroLib.sml
+++ b/realZeroLib.sml
@@ -103,7 +103,7 @@ struct
       val diffP2 = Parse.Term ‘diff ^diffP’ |> EVAL
       val _ = print "Starting Sturm Sequence computation"
       val sseq_aux = decls "sturm_seq_aux";
-      val _ = computeLib.monitoring := SOME (same_const (hd sseq_aux))
+      (* val _ = computeLib.monitoring := SOME (same_const (hd sseq_aux)) *)
       val sseqOpt = Parse.Term ‘sturm_seq ^diffP (diff ^diffP)’ |> EVAL
       val sseq = appOrErr optionSyntax.is_some optionSyntax.dest_some (sseqOpt |> concl |> rhs) "Sturm sequence computation failed"
       val th = MATCH_MP sturm_seq_equiv sseqOpt
@@ -148,7 +148,6 @@ struct
       "[" ^ TextIO.inputAll(instr) ^ "]:(real#real) list"
     end;
 
-
   (** Takes as input a term of the form ! x. x IN ... ==> poly p x <= eps and
       checks it by using the Sollya tool to infer zeros **)
   fun REAL_ZERO_CONV (t:term) =
@@ -157,7 +156,8 @@ struct
       val (pre, conc) = appOrErr is_imp dest_imp imp "Input term not of the form ! x. _ ==> _"
       val (lb, ub) = extractDom pre var
       val dom = Parse.Term ‘(^lb, ^ub)’
-      val (polyApp, eps) = appOrErr realSyntax.is_leq realSyntax.dest_leq conc "Input term not of the form ! x. pre ==> _ <= _"
+      val (polyAppAbs, eps) = appOrErr realSyntax.is_leq realSyntax.dest_leq conc "Input term not of the form ! x. pre ==> _ <= _"
+      val polyApp = rand polyAppAbs
       val (poly, var) = strip_comb polyApp |> snd |> (fn ts => (hd ts, hd (tl ts)))
       val polyDiff = Parse.Term ‘diff ^poly’ |> EVAL
       val (zerosThm, numZeros) = STURM_SEQ_CONV (polyDiff |> concl |> rhs) dom
@@ -196,13 +196,15 @@ struct
     if is_real_const t then
       let val pEqThm = EVAL o Parse.Term $ ‘cst ^t’ in
         (Q.SPECL [‘^t’, ‘^x’] polyEvalsTo_Const
-        |> REWRITE_RULE [pEqThm],
+        |> REWRITE_RULE [pEqThm]
+        |> CONV_RULE $ RATOR_CONV $ RATOR_CONV $ RAND_CONV EVAL,
           pEqThm)
       end
     else if is_var t then
       let val pEqThm = var1_thm in
         (Q.SPECL [‘1’, ‘^t’] (GEN “n:num” polyEvalsTo_Var)
-        |> REWRITE_RULE [var1_thm, POW_1],
+        |> REWRITE_RULE [var1_thm, POW_1]
+        |> CONV_RULE $ RATOR_CONV $ RATOR_CONV $ RAND_CONV EVAL,
           pEqThm)
       end
     else if realSyntax.is_plus t then
@@ -213,7 +215,8 @@ struct
         val pEqThm = EVAL o Parse.Term $ ‘^(p1 |> concl |> rhs) +p ^(p2 |> concl |> rhs)’
       in
         (MATCH_MP (MATCH_MP polyEvalsTo_Add thm1) thm2
-         |> REWRITE_RULE [pEqThm],
+         |> REWRITE_RULE [pEqThm]
+         |> CONV_RULE $ RATOR_CONV $ RATOR_CONV $ RAND_CONV EVAL,
           pEqThm)
       end
     else if realSyntax.is_minus t then
@@ -224,7 +227,8 @@ struct
         val pEqThm = EVAL o Parse.Term $ ‘^(p1 |> concl |> rhs) +p ^(p2 |> concl |> rhs)’
       in
         (MATCH_MP (MATCH_MP polyEvalsTo_Sub thm1) thm2
-         |> REWRITE_RULE [pEqThm],
+         |> REWRITE_RULE [pEqThm]
+         |> CONV_RULE $ RATOR_CONV $ RATOR_CONV $ RAND_CONV EVAL,
           pEqThm)
       end
     else if realSyntax.is_mult t then
@@ -235,7 +239,8 @@ struct
         val pEqThm = EVAL o Parse.Term $ ‘^(p1 |> concl |> rhs) *p ^(p2 |> concl |> rhs)’
       in
         (MATCH_MP (MATCH_MP polyEvalsTo_Mul thm1) thm2
-         |> REWRITE_RULE [pEqThm],
+         |> REWRITE_RULE [pEqThm]
+         |> CONV_RULE $ RATOR_CONV $ RATOR_CONV $ RAND_CONV EVAL,
           pEqThm)
       end
     else if realSyntax.is_negated t then
@@ -245,7 +250,8 @@ struct
         val pEqThm = EVAL o Parse.Term $ ‘--p ^(p1 |> concl |> rhs)’
       in
         (MATCH_MP polyEvalsTo_Neg thm1
-         |> REWRITE_RULE [pEqThm],
+         |> REWRITE_RULE [pEqThm]
+         |> CONV_RULE $ RATOR_CONV $ RATOR_CONV $ RAND_CONV EVAL,
           pEqThm)
       end
     else raise ZeroLibErr "Unsupported term";
@@ -380,7 +386,7 @@ struct
     else let
       val polyErrThm =
         (testSollya();
-         REAL_ZERO_CONV (Parse.Term ‘! x. FST (^ivTm) <= x /\ x <= SND (^ivTm) ==> evalPoly ^errorp x <= ^eps - ^err’))
+         REAL_ZERO_CONV (Parse.Term ‘! x. FST (^ivTm) <= x /\ x <= SND (^ivTm) ==> abs (evalPoly ^errorp x) <= ^eps - ^err’))
       val polyErrThm_simped = REWRITE_RULE [GSYM errorpThm, eval_simps,
                                             GSYM poly_compat, Once $ GSYM transpGetThm,
                                             Once $ GSYM iv_FST, transpThm, optionGet_SOME] polyErrThm
@@ -389,7 +395,39 @@ struct
       (save_thm ("err_sound_thm", final_thm); final_thm)
     end end;
 
+  fun REAL_INEQ_CONV (t:term) = let
+    val (var, tm) = appOrErr is_forall dest_forall t "Not a universally quantified statement"
+    val (pre, conc) = appOrErr is_imp dest_imp tm "Input term not of the form ! x. _ ==> _"
+    val (ltm, rtm) = appOrErr realSyntax.is_leq realSyntax.dest_leq conc "Conclusion not a <= expression"
+    in
+    if not (type_of var = “:real”) then raise ZeroLibErr "Only real number expressions are supported"
+    else let
+      val isAbs = realSyntax.is_absval ltm
+      val argTm = if isAbs then rand ltm else ltm
+      val (evalThm, _) = reflect (Parse.Term ‘^argTm :real’) var
+      val evalRwThm = evalThm |> REWRITE_RULE [polyEvalsTo_def, poly_compat]
+      val theTerm = if isAbs then t else “∀ ^(var). ^pre ⇒ abs ^argTm ≤ ^rtm”
+    in
+      (REAL_ZERO_CONV (REWRITE_CONV [GSYM evalRwThm ] theTerm |> rhs o concl)
+        |> SPEC var
+        |> REWRITE_RULE [evalRwThm]
+        |> GEN_ALL, isAbs, ltm)
+    end end;
+
+  fun REAL_INEQ_TAC (asl, g) =
+    let val (ineqThm, isAbs, ltm) = REAL_INEQ_CONV g in
+    if isAbs then MATCH_ACCEPT_TAC ineqThm (asl, g)
+    else (assume_tac ineqThm
+          >> rpt strip_tac >> irule REAL_LE_TRANS >> qexists_tac ‘abs ^ltm’ >> conj_tac >> gs[ABS_LE]) (asl, g)
+                                                                                                       end;
   (** Some tests **)
+(*
+Theorem test:
+! x. -1 <= x /\ x <= 2 ==> (x * x * x + x * x - 4 * x) <= 4:real
+Proof
+  REAL_INEQ_TAC
+QED
+  *)
   (* reflect “~ ((x + 1/2):real) * x” “x:real” *)
   (* val t = REAL_ZERO_CONV “! x. 90 <= x /\ x <= 100 ==> evalPoly [1; 2/100; 3] x <= 100:real” *)
 
diff --git a/scripts/generate_daisy_certificates.sh b/scripts/generate_daisy_certificates.sh
index e74707ff8b312bd670f807feb6b4de03b5a3bf10..c928148fa5b8062353b72de190b99892e124e5f6 100755
--- a/scripts/generate_daisy_certificates.sh
+++ b/scripts/generate_daisy_certificates.sh
@@ -1,11 +1,32 @@
 #!/bin/bash
 
+PRECISION="23"
+
 cd /home/hbecker/Projects/AVA_Daisy/
 shopt -s nullglob
 sbt compile && sbt script
 for f in ./testcases/transcendentals/*;
 do
-  ./daisy --sollya --certificate=hol4 $f
+  echo $f
+  ./daisy --sollya --Sollya-Precision="$PRECISION" --certificate=hol4 $f
+done
+
+for f in ./testcases/approx/*;
+do
+  echo $f
+  ./daisy --sollya --Sollya-Precision="$PRECISION" --certificate=hol4 $f
+done
+
+for f in ./testcases/fpbench/*;
+do
+  echo $f
+  ./daisy --sollya --Sollya-Precision="$PRECISION" --certificate=hol4 $f
+done
+
+for f in ./testcases/fpbench_separate/*;
+do
+  echo $f
+  ./daisy --sollya --Sollya-Precision="$PRECISION" --certificate=hol4 $f
 done
 
 cp /home/hbecker/Projects/AVA_Daisy/output/cert_* /home/hbecker/Projects/Dandelion/testcases/timing/
diff --git a/scripts/timing.sh b/scripts/timing.sh
index 79b3a956aee867f4dde7add0cd4826e9560c225c..ed98786279c4722b3f22ce1903ce69a0cd7df3e3 100755
--- a/scripts/timing.sh
+++ b/scripts/timing.sh
@@ -5,7 +5,7 @@ LBR=$'\n'
 CURRLINE=""
 #timeout of 1.5 hours = 5400 seconds
 #debugging: timeout of 60 seconds
-TIMEOUT="3600s"
+TIMEOUT="1200s"
 
 if [ "$CMLDIR" = "" ];
 then
@@ -26,10 +26,8 @@ echo "$FLOVERDIR"
 #define some functions:
 function runHOL4 () {
 
-  echo "$TIMEOUT"
-
   # For each Holmake run, we clean, then compile and measure running time
-  Holmake -j1 clean
+  Holmake -j1 -q clean
 
   #First timing measure
   RES1="$( { /usr/bin/time -f "%e" -a /bin/timeout "$TIMEOUT" Holmake -j1 "$1"; } 2>"/tmp/time_$1.txt")"
@@ -41,7 +39,7 @@ function runHOL4 () {
   fi
 
   # clean
-  Holmake -j1 clean
+  Holmake -j1 -q clean
 
   #Second timing measure
   RES2="$( { /usr/bin/time -f "%e" -a /bin/timeout "$TIMEOUT" Holmake -j1 "$1"; } 2>"/tmp/time_$1.txt")"
@@ -53,7 +51,7 @@ function runHOL4 () {
   fi
 
   # clean
-  Holmake -j1 clean
+  Holmake -j1 -q clean
 
   #Third timing measure
   RES3="$( { /usr/bin/time -f "%e" -a /bin/timeout "$TIMEOUT" Holmake -j1 "$1"; } 2>"/tmp/time_$1.txt")"
@@ -95,10 +93,10 @@ do
   #Drop cert_ from table result
   CURRLINE="${FNAME/cert_/}, "
 
-  if ! runHOL4 "$THYNAME"
-  then
-    CURRLINE="$CURRLINE TIMEOUT, TIMEOUT, TIMEOUT"
-  fi
+  #if ! runHOL4 "$THYNAME"
+  #then
+  #  CURRLINE="$CURRLINE TIMEOUT, TIMEOUT, TIMEOUT"
+  #fi
 
   #Now switch to using the binary
   sed -i -r -e 's/useBinary := false/useBinary := true/g' "$f"
diff --git a/testcases/timing/cert_axisRotationX_cosScript.sml b/testcases/timing/cert_axisRotationX_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..ce2eab114fc21724baa40d68dea07fafb62d97ca
--- /dev/null
+++ b/testcases/timing/cert_axisRotationX_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_axisRotationX_cos";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "theta");
+    poly := [
+    (2097169)/(2097152);
+    (-5285315)/(17179869184);
+    (-8349665)/(16777216);
+    (-1787835)/(268435456);
+    (3389287)/(67108864);
+    (-5970771)/(1073741824)
+    ];
+  eps := (10667810060499641756895072302472422990957022994561)/(2000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_axisRotationX_sinScript.sml b/testcases/timing/cert_axisRotationX_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..d19e7c64f67cfaa1bc6437ad14b44d0ba0e95e5e
--- /dev/null
+++ b/testcases/timing/cert_axisRotationX_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_axisRotationX_sin";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "theta");
+    poly := [
+    (4118863)/(549755813888);
+    (4193183)/(4194304);
+    (4009913)/(2147483648);
+    (-2877369)/(16777216);
+    (5861875)/(1073741824);
+    (6346265)/(1073741824)
+    ];
+  eps := (50212791961457274158431077054229880298681030861107)/(10000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_axisRotationY_cosScript.sml b/testcases/timing/cert_axisRotationY_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..5f013c52a05864185960a2667d61b51eef593a5d
--- /dev/null
+++ b/testcases/timing/cert_axisRotationY_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_axisRotationY_cos";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "theta");
+    poly := [
+    (2097169)/(2097152);
+    (-5285315)/(17179869184);
+    (-8349665)/(16777216);
+    (-1787835)/(268435456);
+    (3389287)/(67108864);
+    (-5970771)/(1073741824)
+    ];
+  eps := (10667810060499641756895072302472422990957022994561)/(2000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_axisRotationY_sinScript.sml b/testcases/timing/cert_axisRotationY_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..5d27046fb5320da14b7fb0074033408383a36ebf
--- /dev/null
+++ b/testcases/timing/cert_axisRotationY_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_axisRotationY_sin";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "theta");
+    poly := [
+    (4118863)/(549755813888);
+    (4193183)/(4194304);
+    (4009913)/(2147483648);
+    (-2877369)/(16777216);
+    (5861875)/(1073741824);
+    (6346265)/(1073741824)
+    ];
+  eps := (50212791961457274158431077054229880298681030861107)/(10000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_azimuth_atanScript.sml b/testcases/timing/cert_azimuth_atanScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..0f25a43fc63f3cd4535d3d2f2b3c274763c44a1d
--- /dev/null
+++ b/testcases/timing/cert_azimuth_atanScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_azimuth_atan";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition atan_example_def:
+  atan_example =
+  <|
+    transc := Fun Atn (Var "_tmp1");
+    poly := [
+    (-262953)/(36028797018963968);
+    (9477)/(16384);
+    (1243437)/(144115188075855872);
+    (-7397487)/(536870912);
+    (-45365734823235581707479013857664540410041809082031)/(100000000000000000000000000000000000000000000000000000000000000);
+    (974495)/(8589934592)
+    ];
+  eps := (112038691386080820341959996686064916901956943583897)/(500000000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp1",
+    ((-10020221492936158063531838401233967941897158656)/(1139896108513103022459289132954062320003592137),
+    (10020221492936158063531838401233967941897158656)/(1139896108513103022459289132954062320003592137)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert atan_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_azimuth_cosScript.sml b/testcases/timing/cert_azimuth_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..dcc9a0a2c0c89c21bcfc7680f47e65090f744843
--- /dev/null
+++ b/testcases/timing/cert_azimuth_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_azimuth_cos";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "lat1");
+    poly := [
+    (1)/(1);
+    (-6214527)/(17592186044416);
+    (-524275)/(1048576);
+    (-2440775)/(17179869184);
+    (5688057)/(134217728);
+    (-6989197)/(4294967296)
+    ];
+  eps := (21637462578484117267785355156862147429371953103883)/(5000000000000000000000000000000000000000000000000000000000) ;
+  iv := [("lat1",
+    ((0)/(1),
+    (2)/(5)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_azimuth_sinScript.sml b/testcases/timing/cert_azimuth_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..8e44387f7eec6b71df3cabe140b21d4ba6744dff
--- /dev/null
+++ b/testcases/timing/cert_azimuth_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_azimuth_sin";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "lat1");
+    poly := [
+    (3739177)/(4503599627370496);
+    (8388607)/(8388608);
+    (3317189)/(1099511627776);
+    (-1398339)/(8388608);
+    (7992151)/(68719476736);
+    (2186531)/(268435456)
+    ];
+  eps := (18493509496797928162175721681946815848203685536007)/(20000000000000000000000000000000000000000000000000000000000) ;
+  iv := [("lat1",
+    ((0)/(1),
+    (2)/(5)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_carthesianToPolar_radius_sqrtScript.sml b/testcases/timing/cert_carthesianToPolar_radius_sqrtScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..1faaef7e96580a69f379ca66540d2bf77fcc676e
--- /dev/null
+++ b/testcases/timing/cert_carthesianToPolar_radius_sqrtScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_carthesianToPolar_radius_sqrt";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition sqrt_example_def:
+  sqrt_example =
+  <|
+    transc := Fun Sqrt (Var "_tmp");
+    poly := [
+    (1263771)/(262144);
+    (4304169)/(134217728);
+    (-3703979)/(549755813888);
+    (6929461)/(9007199254740992);
+    (-19823278083050052678082408874615794047713279724121)/(500000000000000000000000000000000000000000000000000000000000000);
+    (74454713051535845446402342440173072191100800409913)/(100000000000000000000000000000000000000000000000000000000000000000000)
+    ];
+  eps := (369783601116367338089620724880429745098032284093)/(100000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp",
+    ((2)/(1),
+    (20000)/(1)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sqrt_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_complex_sine_cosine_expScript.sml b/testcases/timing/cert_complex_sine_cosine_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..0398019646f8df55052dd9ef6a4dbde31765e5a7
--- /dev/null
+++ b/testcases/timing/cert_complex_sine_cosine_expScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_complex_sine_cosine_exp";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "im");
+    poly := [
+    (694783)/(1024);
+    (2316493)/(4096);
+    (-6724885)/(65536);
+    (-240043)/(8192);
+    (8128949)/(4194304);
+    (5814959)/(16777216)
+    ];
+  eps := (4952536921121247330536513070405928094083173015919)/(4000000000000000000000000000000000000000000000) ;
+  iv := [("im",
+    ((-10)/(1),
+    (10)/(1)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_complex_sine_cosine_sinScript.sml b/testcases/timing/cert_complex_sine_cosine_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..353986a7f66799d7199cf0f5f93aaf326efb08c8
--- /dev/null
+++ b/testcases/timing/cert_complex_sine_cosine_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_complex_sine_cosine_sin";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "re");
+    poly := [
+    (-3490547)/(562949953421312);
+    (5960521)/(536870912);
+    (5995701)/(2251799813685248);
+    (-7829763)/(8589934592);
+    (-7293881)/(72057594037927936);
+    (6830413)/(549755813888)
+    ];
+  eps := (9862119842611468515130875712482545208412836134847)/(10000000000000000000000000000000000000000000000000) ;
+  iv := [("re",
+    ((-10)/(1),
+    (10)/(1)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_complex_square_root_sqrtScript.sml b/testcases/timing/cert_complex_square_root_sqrtScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..c67ae48ac9d245566b8dfaba9f135c2f0fa45649
--- /dev/null
+++ b/testcases/timing/cert_complex_square_root_sqrtScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_complex_square_root_sqrt";
+
+val _ = realZeroLib.useBinary := true;
+
+Definition sqrt_example_def:
+  sqrt_example =
+  <|
+    transc := Fun Sqrt (Var "_tmp1");
+    poly := [
+    (6622035)/(16777216);
+    (5636661)/(16777216);
+    (-7831449)/(1073741824);
+    (5798267)/(68719476736);
+    (-3851737)/(8796093022208);
+    (3719839)/(4503599627370496)
+    ];
+  eps := (41811226599957374116083359795898439930906859513429)/(100000000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp1",
+    ((1)/(500000),
+    (200)/(1)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sqrt_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_compundExp2_cosScript.sml b/testcases/timing/cert_compundExp2_cosScript.sml
index b1735476187e020e867c3629344a22d9bd267c7a..f3d3148ea4b300cd7c4ebba92c05b83b0644a5ba 100644
--- a/testcases/timing/cert_compundExp2_cosScript.sml
+++ b/testcases/timing/cert_compundExp2_cosScript.sml
@@ -10,14 +10,14 @@ Definition cos_example_def:
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49499786113949550969692836588365025818347930908203)/(50000000000000000000000000000000000000000000000000);
-    (128085858635211772421635956220598018262535333633423)/(5000000000000000000000000000000000000000000000000000);
-    (-2590775074099603558774873590664356015622615814209)/(5000000000000000000000000000000000000000000000000);
-    (-28521974777214653597873228463299710710998624563217)/(5000000000000000000000000000000000000000000000000000);
-    (55755996420433367316560335780195600818842649459839)/(1000000000000000000000000000000000000000000000000000);
-    (-72250184799853610709274853718397935153916478157043)/(10000000000000000000000000000000000000000000000000000)
+    (4152343)/(4194304);
+    (6876525)/(268435456);
+    (-4346597)/(8388608);
+    (-3062641)/(536870912);
+    (7483453)/(134217728);
+    (-3878907)/(536870912)
     ];
-  eps := (17901045018330561497426731620288681891391631699211)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (17903735461153006055494631482825567465408993566057)/(1000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(1),
     (3)/(1)))];
diff --git a/testcases/timing/cert_compundExp2_expScript.sml b/testcases/timing/cert_compundExp2_expScript.sml
index 02753db2a0ce6a4d76dde128b8b4eeb1c79b4378..4e744d0c8717f61980efb3d1a1cd9f1c9dcec711 100644
--- a/testcases/timing/cert_compundExp2_expScript.sml
+++ b/testcases/timing/cert_compundExp2_expScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_compundExp2_exp";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition exp_example_def:
   exp_example =
   <|
     transc := Fun Exp (Var "_tmp6");
     poly := [
-    (49903705232862027862950071721570566296577453613281)/(50000000000000000000000000000000000000000000000000);
-    (50051295977424398175870123850472737103700637817383)/(50000000000000000000000000000000000000000000000000);
-    (10214838893612917525288708020525518804788589477539)/(20000000000000000000000000000000000000000000000000);
-    (42266092434857821524829546433466020971536636352539)/(250000000000000000000000000000000000000000000000000);
-    (16970862570705050678676606423778139287605881690979)/(500000000000000000000000000000000000000000000000000);
-    (29838937212723814964426827245347340067382901906967)/(10000000000000000000000000000000000000000000000000000)
+    (2093113)/(2097152);
+    (4198607)/(4194304);
+    (2142207)/(4194304);
+    (5672859)/(33554432);
+    (2277791)/(67108864);
+    (3203933)/(1073741824)
     ];
-  eps := (384228340048699048562321505226710078692309137271)/(125000000000000000000000000000000000000000000000000) ;
+  eps := (30737787590925082356054193684126485379075352418331)/(10000000000000000000000000000000000000000000000000000) ;
   iv := [("_tmp6",
     ((-7911935063232343)/(2251799813685248),
     (4441905629231941)/(4503599627370496)))];
diff --git a/testcases/timing/cert_compundExp2_sinScript.sml b/testcases/timing/cert_compundExp2_sinScript.sml
index fa3e068cd66c7d0b50e46b5a294d1aa0444d6db3..4835887c1e8343e32250a105583185db7a0ace4c 100644
--- a/testcases/timing/cert_compundExp2_sinScript.sml
+++ b/testcases/timing/cert_compundExp2_sinScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_compundExp2_sin";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition sin_example_def:
   sin_example =
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (121419254010413)/(2251799813685248);
-    (81328606860352142815528964092663954943418502807617)/(100000000000000000000000000000000000000000000000000);
-    (6494149570753833533576226955119636841118335723877)/(25000000000000000000000000000000000000000000000000);
-    (-8781323325107194543992505941787385381758213043213)/(25000000000000000000000000000000000000000000000000);
-    (4318446802657493512056507967145080328918993473053)/(62500000000000000000000000000000000000000000000000);
-    (-33061430821752406730706930204632953973487019538879)/(10000000000000000000000000000000000000000000000000000)
+    (7237239)/(134217728);
+    (6822323)/(8388608);
+    (2179091)/(8388608);
+    (-5893063)/(16777216);
+    (2318457)/(33554432);
+    (-7099943)/(2147483648)
     ];
-  eps := (38184063150069103085767272755264527270119675555123)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (19091772595121090156795670799594146314679365632711)/(500000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(1),
     (3)/(1)))];
diff --git a/testcases/timing/cert_compundExp_cosScript.sml b/testcases/timing/cert_compundExp_cosScript.sml
index c97029ee07b3f4e01e22143f0bdfbdae74350589..7efe4545e21aed6a0e9f4c3881c56c87feacd41c 100644
--- a/testcases/timing/cert_compundExp_cosScript.sml
+++ b/testcases/timing/cert_compundExp_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_compundExp_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49499786113949550969692836588365025818347930908203)/(50000000000000000000000000000000000000000000000000);
-    (128085858635211772421635956220598018262535333633423)/(5000000000000000000000000000000000000000000000000000);
-    (-2590775074099603558774873590664356015622615814209)/(5000000000000000000000000000000000000000000000000);
-    (-28521974777214653597873228463299710710998624563217)/(5000000000000000000000000000000000000000000000000000);
-    (55755996420433367316560335780195600818842649459839)/(1000000000000000000000000000000000000000000000000000);
-    (-72250184799853610709274853718397935153916478157043)/(10000000000000000000000000000000000000000000000000000)
+    (4152343)/(4194304);
+    (6876525)/(268435456);
+    (-4346597)/(8388608);
+    (-3062641)/(536870912);
+    (7483453)/(134217728);
+    (-3878907)/(536870912)
     ];
-  eps := (17901045018330561497426731620288681891391631699211)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (17903735461153006055494631482825567465408993566057)/(1000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(1),
     (3)/(1)))];
diff --git a/testcases/timing/cert_compundExp_expScript.sml b/testcases/timing/cert_compundExp_expScript.sml
index 20e24dc9885f293cb916a24b337b0cd6b2101ce2..7e3f2509c8b726994759123e557b2a5398d41148 100644
--- a/testcases/timing/cert_compundExp_expScript.sml
+++ b/testcases/timing/cert_compundExp_expScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_compundExp_exp";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition exp_example_def:
   exp_example =
   <|
     transc := Fun Exp (Var "_tmp");
     poly := [
-    (49906260036007690783499413100798847153782844543457)/(50000000000000000000000000000000000000000000000000);
-    (1129704292730985)/(1125899906842624);
-    (12778448310462493797690086694274214096367359161377)/(25000000000000000000000000000000000000000000000000);
-    (8273749286506178884925688521434494759887456893921)/(50000000000000000000000000000000000000000000000000);
-    (31621026498711700403188018526634550653398036956787)/(1000000000000000000000000000000000000000000000000000);
-    (5201636942015844602971164079008303815498948097229)/(2000000000000000000000000000000000000000000000000000)
+    (8372881)/(8388608);
+    (1052119)/(1048576);
+    (535967)/(1048576);
+    (2776211)/(16777216);
+    (2122053)/(67108864);
+    (1396305)/(536870912)
     ];
-  eps := (8028271047844550362936034057013566095237518667107)/(2500000000000000000000000000000000000000000000000000) ;
+  eps := (16056374647763546361991814788317828028927266863643)/(5000000000000000000000000000000000000000000000000000) ;
   iv := [("_tmp",
     ((-16919134317973335)/(4503599627370496),
     (1033500435770049)/(1125899906842624)))];
diff --git a/testcases/timing/cert_compundExp_sinScript.sml b/testcases/timing/cert_compundExp_sinScript.sml
index d8fbe6292a6fdca1cf9999d83a3eb8f692b1d3fd..36f0a18a65834c8be7ab152d4224d69ceb2c0fcd 100644
--- a/testcases/timing/cert_compundExp_sinScript.sml
+++ b/testcases/timing/cert_compundExp_sinScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_compundExp_sin";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition sin_example_def:
   sin_example =
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (121419254010413)/(2251799813685248);
-    (81328606860352142815528964092663954943418502807617)/(100000000000000000000000000000000000000000000000000);
-    (6494149570753833533576226955119636841118335723877)/(25000000000000000000000000000000000000000000000000);
-    (-8781323325107194543992505941787385381758213043213)/(25000000000000000000000000000000000000000000000000);
-    (4318446802657493512056507967145080328918993473053)/(62500000000000000000000000000000000000000000000000);
-    (-33061430821752406730706930204632953973487019538879)/(10000000000000000000000000000000000000000000000000000)
+    (7237239)/(134217728);
+    (6822323)/(8388608);
+    (2179091)/(8388608);
+    (-5893063)/(16777216);
+    (2318457)/(33554432);
+    (-7099943)/(2147483648)
     ];
-  eps := (38184063150069103085767272755264527270119675555123)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (19091772595121090156795670799594146314679365632711)/(500000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(1),
     (3)/(1)))];
diff --git a/testcases/timing/cert_cosine_cosScript.sml b/testcases/timing/cert_cosine_cosScript.sml
index c3ad89c21995e99f6648a7a874b29f42a018c61d..3909de5f51502af6d92d9765965e6106cf10d97d 100644
--- a/testcases/timing/cert_cosine_cosScript.sml
+++ b/testcases/timing/cert_cosine_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_cosine_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49970161473570773313923609748599119484424591064453)/(50000000000000000000000000000000000000000000000000);
-    (6498981876590578766710488801920082922291416194227)/(2000000000000000000000000000000000000000000000000000000000000);
-    (-24779042460787940871380641283394652418792247772217)/(50000000000000000000000000000000000000000000000000);
-    (-36590953272492754955052397704507867698224543584473)/(10000000000000000000000000000000000000000000000000000000000000);
-    (36791682797582943298397850639958051033318042755127)/(1000000000000000000000000000000000000000000000000000);
-    (2373070043805035965109487885352540033530050617161)/(2500000000000000000000000000000000000000000000000000000000000)
+    (4191801)/(4194304);
+    (468303)/(144115188075855872);
+    (-8314467)/(16777216);
+    (-4218665)/(1152921504606846976);
+    (308631)/(8388608);
+    (1094389)/(1152921504606846976)
     ];
-  eps := (10422499708057265669949761692307192664550007378397)/(10000000000000000000000000000000000000000000000000000) ;
+  eps := (521124111034269599864885315659928956893966796293)/(500000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-157079632679)/(100000000000),
     (157079632679)/(100000000000)))];
diff --git a/testcases/timing/cert_e1_expScript.sml b/testcases/timing/cert_e1_expScript.sml
index 3dbe192b67d3e42ab0a407a21e056bbd5f168d7e..276f97d211ab3bacee2fef07f7dd521b0bd153bb 100644
--- a/testcases/timing/cert_e1_expScript.sml
+++ b/testcases/timing/cert_e1_expScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_e1_exp";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition exp_example_def:
   exp_example =
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (4999999931796150209883933257515309378504753112793)/(5000000000000000000000000000000000000000000000000);
-    (50000097063590825952061891257471870630979537963867)/(50000000000000000000000000000000000000000000000000);
-    (1562360245421577295554804720723041100427508354187)/(3125000000000000000000000000000000000000000000000);
-    (8352107336261218456519017649952729698270559310913)/(50000000000000000000000000000000000000000000000000);
-    (1257917021031169967429375056156004575314000248909)/(31250000000000000000000000000000000000000000000000);
-    (107320975289066176255881046586182492319494485855103)/(10000000000000000000000000000000000000000000000000000)
+    (1)/(1);
+    (2097155)/(2097152);
+    (8387951)/(16777216);
+    (1401041)/(8388608);
+    (5409375)/(134217728);
+    (5742483)/(536870912)
     ];
-  eps := (16611710139761674573970861900969344865357465613843)/(1000000000000000000000000000000000000000000000000000000000) ;
+  eps := (9100089594824668833123882767022295764606307420863)/(500000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (1)/(2)))];
diff --git a/testcases/timing/cert_ex2_10_cosScript.sml b/testcases/timing/cert_ex2_10_cosScript.sml
index f83da1ef591e010562e7ad368a082d28334fec66..312a56ec1439a93bc1334033bba9268002f72b42 100644
--- a/testcases/timing/cert_ex2_10_cosScript.sml
+++ b/testcases/timing/cert_ex2_10_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_10_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (8475997234036611)/(1099511627776);
-    (15878712574744367)/(8796093022208);
-    (11584099263717019)/(70368744177664);
-    (72512314317539687813507498503895476460456848144531)/(10000000000000000000000000000000000000000000000000);
-    (15229817333452369543245197291980730369687080383301)/(100000000000000000000000000000000000000000000000000);
-    (59535796806572385472811070883381034946069121360779)/(50000000000000000000000000000000000000000000000000000)
+    (7891721)/(1024);
+    (7391779)/(4096);
+    (5392275)/(32768);
+    (7600053)/(1048576);
+    (5107353)/(33554432);
+    (1277519)/(1073741824)
     ];
-  eps := (5924185653987560103376101374204431204313385859239)/(10000000000000000000000000000000000000000000000000) ;
+  eps := (2960777586449059173561601714215515649805952000053)/(5000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-20)/(1),
     (-18)/(1)))];
diff --git a/testcases/timing/cert_ex2_10_sinScript.sml b/testcases/timing/cert_ex2_10_sinScript.sml
index 98d55909e596172417caa653f6eac2c2d73b8dfb..14370627d1c9f7eb84d37f5ad8799193e4e83c65 100644
--- a/testcases/timing/cert_ex2_10_sinScript.sml
+++ b/testcases/timing/cert_ex2_10_sinScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_10_sin";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition sin_example_def:
   sin_example =
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (2420257326997291)/(137438953472);
-    (10523554368687037)/(2199023255552);
-    (9096720795091875)/(17592186044416);
-    (15631086398117075)/(562949953421312);
-    (37048617350744106335724836753797717392444610595703)/(50000000000000000000000000000000000000000000000000);
-    (7862310969379565292469713710943324258551001548767)/(1000000000000000000000000000000000000000000000000000)
+    (4507533)/(256);
+    (4899869)/(1024);
+    (2117781)/(4096);
+    (3639059)/(131072);
+    (194225)/(262144);
+    (4220719)/(536870912)
     ];
-  eps := (2074874948072183895441013918565864111853128809109)/(1000000000000000000000000000000000000000000000000) ;
+  eps := (10369143912710158366269051986493613696607443283479)/(5000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-20)/(1),
     (-18)/(1)))];
diff --git a/testcases/timing/cert_ex2_11_cosScript.sml b/testcases/timing/cert_ex2_11_cosScript.sml
index 831d9ff3fa301b56bf202df666b8586c89b346bb..82e121428b1eaab5039a1944aae3c1ce1a040d49 100644
--- a/testcases/timing/cert_ex2_11_cosScript.sml
+++ b/testcases/timing/cert_ex2_11_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_11_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (6249783381158049988535196916927816346287727355957)/(6250000000000000000000000000000000000000000000000);
-    (13994891901491600253500807715667519914859440177679)/(100000000000000000000000000000000000000000000000000000);
-    (-12483966310150999140526906217019131872802972793579)/(25000000000000000000000000000000000000000000000000);
-    (-38240818961948281002119487403945186088094487786293)/(50000000000000000000000000000000000000000000000000000);
-    (39826343106799045462595998401411634404212236404419)/(1000000000000000000000000000000000000000000000000000);
-    (15862744354085818411156938445571995544014498591423)/(20000000000000000000000000000000000000000000000000000)
+    (8388317)/(8388608);
+    (4808333)/(34359738368);
+    (-4188923)/(8388608);
+    (-410581)/(536870912);
+    (1336347)/(33554432);
+    (3406261)/(4294967296)
     ];
-  eps := (1023441697182930881414149675607332533469539127847)/(15625000000000000000000000000000000000000000000000000) ;
+  eps := (65529303758252455671868215545661298336506206840853)/(1000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-11)/(10),
     (9)/(10)))];
diff --git a/testcases/timing/cert_ex2_11_tanScript.sml b/testcases/timing/cert_ex2_11_tanScript.sml
index 11fd09e9aea69ab22e0dced761b00066b3257123..bea037df6888b7c81aa92de75eff18da596cf772 100644
--- a/testcases/timing/cert_ex2_11_tanScript.sml
+++ b/testcases/timing/cert_ex2_11_tanScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_11_tan";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition tan_example_def:
   tan_example =
   <|
     transc := Fun Tan (Var "x");
     poly := [
-    (47921244957218727669387425827096649300074204802513)/(100000000000000000000000000000000000000000000000000000);
-    (10402796496814009641340703637979459017515182495117)/(10000000000000000000000000000000000000000000000000);
-    (-794939934620530162800999818273339769802987575531)/(100000000000000000000000000000000000000000000000000);
-    (52175259182069368135703513189582736231386661529541)/(500000000000000000000000000000000000000000000000000);
-    (27765683121179801640110440530406776815652847290039)/(2000000000000000000000000000000000000000000000000000);
-    (21295640250989048003482650983642088249325752258301)/(50000000000000000000000000000000000000000000000000)
+    (4116379)/(8589934592);
+    (4363249)/(4194304);
+    (-533473)/(67108864);
+    (3501425)/(33554432);
+    (7453271)/(536870912);
+    (3572815)/(8388608)
     ];
-  eps := (38367348118360945821328275689786203424286076042799)/(5000000000000000000000000000000000000000000000000000) ;
+  eps := (7673470884841900379557518322799672750953333948881)/(1000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-11)/(10),
     (9)/(10)))];
diff --git a/testcases/timing/cert_ex2_12_expScript.sml b/testcases/timing/cert_ex2_12_expScript.sml
index 21ce90fd403a9ce9b4858aa6b870e43c274b4ea6..029063b172d04a0beddd8c7440d31700b8405b56 100644
--- a/testcases/timing/cert_ex2_12_expScript.sml
+++ b/testcases/timing/cert_ex2_12_expScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_12_exp";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition exp_example_def:
   exp_example =
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (9831133757482081)/(281474976710656);
-    (-3829924765706923)/(70368744177664);
-    (-58126890881545945077846226922702044248580932617187)/(10000000000000000000000000000000000000000000000000);
-    (2852337455093138518513740109483478590846061706543)/(1250000000000000000000000000000000000000000000000);
-    (16341408538600293853804146237962413579225540161133)/(50000000000000000000000000000000000000000000000000);
-    (21800995052293933168519046716937737073749303817749)/(2000000000000000000000000000000000000000000000000000)
+    (286123)/(8192);
+    (-3566895)/(65536);
+    (-3047521)/(524288);
+    (1196357)/(524288);
+    (2741633)/(8388608);
+    (5852159)/(536870912)
     ];
-  eps := (22477143972832700719912314797797738822914817670769)/(200000000000000000000000000000000000000000000000) ;
+  eps := (112385742827975277640517490498994829713728167803553)/(1000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-17)/(1),
     (73)/(10)))];
diff --git a/testcases/timing/cert_ex2_1_cosScript.sml b/testcases/timing/cert_ex2_1_cosScript.sml
index 61f36c33800aa6c09531a7244dd1cd87804bab0b..78e83532b214abdfe8c961ff4aeb09e7b194d0ef 100644
--- a/testcases/timing/cert_ex2_1_cosScript.sml
+++ b/testcases/timing/cert_ex2_1_cosScript.sml
@@ -3,24 +3,24 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_1_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49970161473570773313923609748599119484424591064453)/(50000000000000000000000000000000000000000000000000);
-    (6498981876590578766710488801920082922291416194227)/(2000000000000000000000000000000000000000000000000000000000000);
-    (-24779042460787940871380641283394652418792247772217)/(50000000000000000000000000000000000000000000000000);
-    (-36590953272492754955052397704507867698224543584473)/(10000000000000000000000000000000000000000000000000000000000000);
-    (36791682797582943298397850639958051033318042755127)/(1000000000000000000000000000000000000000000000000000);
-    (2373070043805035965109487885352540033530050617161)/(2500000000000000000000000000000000000000000000000000000000000)
+    (8383617)/(8388608);
+    (934019)/(288230376151711744);
+    (-8314613)/(16777216);
+    (-32901)/(9007199254740992);
+    (617341)/(16777216);
+    (4374397)/(4611686018427387904)
     ];
-  eps := (10422499708057265669949761692307192664550007378397)/(10000000000000000000000000000000000000000000000000000) ;
+  eps := (2600318212236202220851978224779701189781834308159)/(2500000000000000000000000000000000000000000000000000) ;
   iv := [("x",
-    ((-157079632679)/(100000000000),
-    (157079632679)/(100000000000)))];
+    ((-157)/(100),
+    (157)/(100)))];
   |>
 End
 
diff --git a/testcases/timing/cert_ex2_1_sinScript.sml b/testcases/timing/cert_ex2_1_sinScript.sml
index 5f24cb1d80b995791daefbf85339d081b0be4c60..a4bf6f6cb20925f647c5bd6a5b9b9b39dc376960 100644
--- a/testcases/timing/cert_ex2_1_sinScript.sml
+++ b/testcases/timing/cert_ex2_1_sinScript.sml
@@ -3,24 +3,24 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_1_sin";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition sin_example_def:
   sin_example =
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-27761522985246471972987058430257085420329865588229)/(10000000000000000000000000000000000000000000000000000000000000);
-    (99969677314052479699668651846877764910459518432617)/(100000000000000000000000000000000000000000000000000);
-    (11536456095163883772080219177679652020444833748769)/(500000000000000000000000000000000000000000000000000000000000);
-    (-165673079310543952535894618449674453586339950561523)/(1000000000000000000000000000000000000000000000000000);
-    (-179764345886510341357370401589800990461293084266003)/(10000000000000000000000000000000000000000000000000000000000000);
-    (75143771680937715765069562223743560025468468666077)/(10000000000000000000000000000000000000000000000000000)
+    (-99651)/(36028797018963968);
+    (1048259)/(1048576);
+    (1658089)/(72057594037927936);
+    (-1389783)/(8388608);
+    (-646575)/(36028797018963968);
+    (2017339)/(268435456)
     ];
-  eps := (16948642788220920879930931195679997582486139089333)/(250000000000000000000000000000000000000000000000000000) ;
+  eps := (1351216662286119992517282238944946966077859959683)/(20000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
-    ((-157079632679)/(100000000000),
-    (157079632679)/(100000000000)))];
+    ((-157)/(100),
+    (157)/(100)))];
   |>
 End
 
diff --git a/testcases/timing/cert_ex2_2_cosScript.sml b/testcases/timing/cert_ex2_2_cosScript.sml
index 45e8c5d8d3400f38cde9dea2d0748e50c9d0a322..ee05ffdb6eb8117a6cea6b745b2b71c25e2cd5b0 100644
--- a/testcases/timing/cert_ex2_2_cosScript.sml
+++ b/testcases/timing/cert_ex2_2_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_2_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (99995812247583759635460864956257864832878112792969)/(100000000000000000000000000000000000000000000000000);
-    (14948868682263788340094758975323376904743855053681)/(50000000000000000000000000000000000000000000000000000000000000);
-    (-12481041752281745588204486807626381050795316696167)/(25000000000000000000000000000000000000000000000000);
-    (-10484778383983895644902297582895193369170987879313)/(12500000000000000000000000000000000000000000000000000000000000);
-    (39627731007533060353376086482057871762663125991821)/(1000000000000000000000000000000000000000000000000000);
-    (5398048970734422966517262635091023179685805477579)/(10000000000000000000000000000000000000000000000000000000000000)
+    (8388257)/(8388608);
+    (29894072243671909738793601718498393893241882324219)/(100000000000000000000000000000000000000000000000000000000000000);
+    (-523493)/(1048576);
+    (-83861986365646457031175486918073147535324096679687)/(100000000000000000000000000000000000000000000000000000000000000);
+    (2659381)/(67108864);
+    (53966889550921548490691748156677931547164916992187)/(100000000000000000000000000000000000000000000000000000000000000)
     ];
-  eps := (41907281284879500810150507052280045622425693494313)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (41912596079773288041891308328911850604299963363941)/(1000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-1)/(1),
     (1)/(1)))];
diff --git a/testcases/timing/cert_ex2_2_sinScript.sml b/testcases/timing/cert_ex2_2_sinScript.sml
index 61d360c98c848182c35f21f8d6f1dc32dec035b2..f3ebbcee41aa1b670d897054925866d1bc151ccc 100644
--- a/testcases/timing/cert_ex2_2_sinScript.sml
+++ b/testcases/timing/cert_ex2_2_sinScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_2_sin";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition sin_example_def:
   sin_example =
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-21599530253946504295057214919429729785814182224657)/(200000000000000000000000000000000000000000000000000000000000000);
-    (99997892514260611207532747357618063688278198242187)/(100000000000000000000000000000000000000000000000000);
-    (43987793637083000398570439942042676175273929750631)/(20000000000000000000000000000000000000000000000000000000000000);
-    (-8324867549409317030173482976351806428283452987671)/(50000000000000000000000000000000000000000000000000);
-    (-2629428451523737722547785850551502033218415066429)/(625000000000000000000000000000000000000000000000000000000000);
-    (39962076698155783206767299731154707842506468296051)/(5000000000000000000000000000000000000000000000000000)
+    (-107589528649046362041019619937287643551826477050781)/(1000000000000000000000000000000000000000000000000000000000000000);
+    (8388431)/(8388608);
+    (2530041)/(1152921504606846976);
+    (-5586721)/(33554432);
+    (-4842627)/(1152921504606846976);
+    (2145429)/(268435456)
     ];
-  eps := (15148894879265446456263448238167392842829276048601)/(5000000000000000000000000000000000000000000000000000000) ;
+  eps := (60548476199915543631442071003381552909832486986057)/(20000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-1)/(1),
     (1)/(1)))];
diff --git a/testcases/timing/cert_ex2_3_cosScript.sml b/testcases/timing/cert_ex2_3_cosScript.sml
index 9ea1627db891e6488916dcc0a8f3a61dadb97078..f6a8063cdf3983e9b4f5890f8a9c0f35ce0f1a87 100644
--- a/testcases/timing/cert_ex2_3_cosScript.sml
+++ b/testcases/timing/cert_ex2_3_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_3_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (1125900571214867)/(1125899906842624);
-    (-42966107257675805787284356584976308113255072385073)/(1000000000000000000000000000000000000000000000000000000);
-    (-49949272499826849469606315778946736827492713928223)/(100000000000000000000000000000000000000000000000000);
-    (-10976010924595921980362334124947665259242057800293)/(5000000000000000000000000000000000000000000000000000);
-    (4598109693814972365188964431581553071737289428711)/(100000000000000000000000000000000000000000000000000);
-    (-3947897779564603533419830938555605825968086719513)/(1000000000000000000000000000000000000000000000000000)
+    (2097153)/(2097152);
+    (-2796561)/(68719476736);
+    (-8380311)/(16777216);
+    (-4651583)/(2147483648);
+    (1541891)/(33554432);
+    (-1056907)/(268435456)
     ];
-  eps := (14938084158257771228202592443201212569907145068827)/(25000000000000000000000000000000000000000000000000000000) ;
+  eps := (30478272337018497341296004076094224199055105829899)/(50000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (1)/(1)))];
diff --git a/testcases/timing/cert_ex2_4_cosScript.sml b/testcases/timing/cert_ex2_4_cosScript.sml
index 9936218306d0b1fe2d6ad77e3de5e85816c73335..d1a1531925edac1beeb817b8785a0495cfbd3ed9 100644
--- a/testcases/timing/cert_ex2_4_cosScript.sml
+++ b/testcases/timing/cert_ex2_4_cosScript.sml
@@ -3,24 +3,24 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_4_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49970161473570773313923609748599119484424591064453)/(50000000000000000000000000000000000000000000000000);
-    (6498981876590578766710488801920082922291416194227)/(2000000000000000000000000000000000000000000000000000000000000);
-    (-24779042460787940871380641283394652418792247772217)/(50000000000000000000000000000000000000000000000000);
-    (-36590953272492754955052397704507867698224543584473)/(10000000000000000000000000000000000000000000000000000000000000);
-    (36791682797582943298397850639958051033318042755127)/(1000000000000000000000000000000000000000000000000000);
-    (2373070043805035965109487885352540033530050617161)/(2500000000000000000000000000000000000000000000000000000000000)
+    (8383617)/(8388608);
+    (934019)/(288230376151711744);
+    (-8314613)/(16777216);
+    (-32901)/(9007199254740992);
+    (617341)/(16777216);
+    (4374397)/(4611686018427387904)
     ];
-  eps := (10422499708057265669949761692307192664550007378397)/(10000000000000000000000000000000000000000000000000000) ;
+  eps := (2600318212236202220851978224779701189781834308159)/(2500000000000000000000000000000000000000000000000000) ;
   iv := [("x",
-    ((-157079632679)/(100000000000),
-    (157079632679)/(100000000000)))];
+    ((-157)/(100),
+    (157)/(100)))];
   |>
 End
 
diff --git a/testcases/timing/cert_ex2_4_sinScript.sml b/testcases/timing/cert_ex2_4_sinScript.sml
index 6b4b70886b4b209aba1ad28b8c9096e531ff4a5b..162b91ee35aa036e02f0c40d78b83c297a35eb6e 100644
--- a/testcases/timing/cert_ex2_4_sinScript.sml
+++ b/testcases/timing/cert_ex2_4_sinScript.sml
@@ -3,24 +3,24 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_4_sin";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition sin_example_def:
   sin_example =
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-27761522985246471972987058430257085420329865588229)/(10000000000000000000000000000000000000000000000000000000000000);
-    (99969677314052479699668651846877764910459518432617)/(100000000000000000000000000000000000000000000000000);
-    (11536456095163883772080219177679652020444833748769)/(500000000000000000000000000000000000000000000000000000000000);
-    (-165673079310543952535894618449674453586339950561523)/(1000000000000000000000000000000000000000000000000000);
-    (-179764345886510341357370401589800990461293084266003)/(10000000000000000000000000000000000000000000000000000000000000);
-    (75143771680937715765069562223743560025468468666077)/(10000000000000000000000000000000000000000000000000000)
+    (-99651)/(36028797018963968);
+    (1048259)/(1048576);
+    (1658089)/(72057594037927936);
+    (-1389783)/(8388608);
+    (-646575)/(36028797018963968);
+    (2017339)/(268435456)
     ];
-  eps := (16948642788220920879930931195679997582486139089333)/(250000000000000000000000000000000000000000000000000000) ;
+  eps := (1351216662286119992517282238944946966077859959683)/(20000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
-    ((-157079632679)/(100000000000),
-    (157079632679)/(100000000000)))];
+    ((-157)/(100),
+    (157)/(100)))];
   |>
 End
 
diff --git a/testcases/timing/cert_ex2_5_cosScript.sml b/testcases/timing/cert_ex2_5_cosScript.sml
index 1bbf3dd9657a9cc682de5babf495b32658271e64..61400752be47f00ea1edd2845a1b74e09e9d418b 100644
--- a/testcases/timing/cert_ex2_5_cosScript.sml
+++ b/testcases/timing/cert_ex2_5_cosScript.sml
@@ -3,21 +3,21 @@ open realZeroLib preambleDandelion;
 
 val _ = new_theory "cert_ex2_5_cos";
 
-val _ = realZeroLib.useBinary := false;
+val _ = realZeroLib.useBinary := true;
 
 Definition cos_example_def:
   cos_example =
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (-12665022292772177)/(1099511627776);
-    (7541462297695337)/(2199023255552);
-    (-7134767594637231)/(17592186044416);
-    (13403885700886967)/(562949953421312);
-    (-34698182848243522280462514117971295490860939025879)/(50000000000000000000000000000000000000000000000000);
-    (20085536140263544457179589741713243711274117231369)/(2500000000000000000000000000000000000000000000000000)
+    (-6076757)/(512);
+    (3613947)/(1024);
+    (-6831249)/(16384);
+    (801477)/(32768);
+    (-747077)/(1048576);
+    (2213309)/(268435456)
     ];
-  eps := (8937978655347983526527714370895553009643740293223)/(500000000000000000000000000000000000000000000000) ;
+  eps := (37366189361456402327252193224779690233235507783359)/(50000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((17)/(1),
     (18)/(1)))];
diff --git a/testcases/timing/cert_ex2_5_sinScript.sml b/testcases/timing/cert_ex2_5_sinScript.sml
index ce9d5b80a2db798407ac64141ac473ad12dafdf8..b758954e692916baee4673fbb3a9efe68b562d35 100644
--- a/testcases/timing/cert_ex2_5_sinScript.sml
+++ b/testcases/timing/cert_ex2_5_sinScript.sml
@@ -10,14 +10,14 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-878307690014483)/(137438953472);
-    (14580053684821893)/(8796093022208);
-    (-739770641893437)/(4398046511104);
-    (10384489919624005915821385315211955457925796508789)/(1250000000000000000000000000000000000000000000000);
-    (-9912947356822587874347618708270601928234100341797)/(50000000000000000000000000000000000000000000000000);
-    (22587609163990134597457121179431283053418155759573)/(12500000000000000000000000000000000000000000000000000)
+    (-1615877)/(256);
+    (6697419)/(4096);
+    (-339225)/(2048);
+    (2139309)/(262144);
+    (-6511689)/(33554432);
+    (7555033)/(4294967296)
     ];
-  eps := (143100364059897487165342130470665345272647186550267)/(50000000000000000000000000000000000000000000000000000000) ;
+  eps := (2942678771268373863625422560015572619487755298937)/(1000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((17)/(1),
     (18)/(1)))];
diff --git a/testcases/timing/cert_ex2_6_tanScript.sml b/testcases/timing/cert_ex2_6_tanScript.sml
index f2a485fb0fdaa236521af26834abc05e0d1bee2a..cf38617193c83f08490829ae2ea670c92f011916 100644
--- a/testcases/timing/cert_ex2_6_tanScript.sml
+++ b/testcases/timing/cert_ex2_6_tanScript.sml
@@ -10,14 +10,14 @@ Definition tan_example_def:
   <|
     transc := Fun Tan (Var "x");
     poly := [
-    (14397187876383914718880192800030634082963931774657)/(100000000000000000000000000000000000000000000000000000000000);
-    (10170286709124173318841144464386161416769027709961)/(10000000000000000000000000000000000000000000000000);
-    (-20595385928462770257067143648893256524523565076379)/(5000000000000000000000000000000000000000000000000000000000);
-    (215234735736637372571777859775465913116931915283203)/(1000000000000000000000000000000000000000000000000000);
-    (8152790215406542887601352227917861359429707590607)/(1000000000000000000000000000000000000000000000000000000000);
-    (32254149779987517643320416027563624083995819091797)/(100000000000000000000000000000000000000000000000000)
+    (5187277)/(36028797018963968);
+    (4265727)/(4194304);
+    (-4637715)/(1125899906842624);
+    (7222091)/(33554432);
+    (4589643)/(562949953421312);
+    (338209)/(1048576)
     ];
-  eps := (1017738418050999142110392094835584939384313101813)/(312500000000000000000000000000000000000000000000000) ;
+  eps := (16283853154200562345701750884649512915292507362897)/(5000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-1)/(1),
     (1)/(1)))];
diff --git a/testcases/timing/cert_ex2_7_cosScript.sml b/testcases/timing/cert_ex2_7_cosScript.sml
index b5f3151bc8e8e765c0d0371e911dd158c0a79f4a..b5868b67fa0c1f1e3d96dfb1cb64eaa53635fe36 100644
--- a/testcases/timing/cert_ex2_7_cosScript.sml
+++ b/testcases/timing/cert_ex2_7_cosScript.sml
@@ -10,17 +10,17 @@ Definition cos_example_def:
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49970161473570773313923609748599119484424591064453)/(50000000000000000000000000000000000000000000000000);
-    (6498981876590578766710488801920082922291416194227)/(2000000000000000000000000000000000000000000000000000000000000);
-    (-24779042460787940871380641283394652418792247772217)/(50000000000000000000000000000000000000000000000000);
-    (-36590953272492754955052397704507867698224543584473)/(10000000000000000000000000000000000000000000000000000000000000);
-    (36791682797582943298397850639958051033318042755127)/(1000000000000000000000000000000000000000000000000000);
-    (2373070043805035965109487885352540033530050617161)/(2500000000000000000000000000000000000000000000000000000000000)
+    (8383617)/(8388608);
+    (934019)/(288230376151711744);
+    (-8314613)/(16777216);
+    (-32901)/(9007199254740992);
+    (617341)/(16777216);
+    (4374397)/(4611686018427387904)
     ];
-  eps := (10422499708057265669949761692307192664550007378397)/(10000000000000000000000000000000000000000000000000000) ;
+  eps := (2600318212236202220851978224779701189781834308159)/(2500000000000000000000000000000000000000000000000000) ;
   iv := [("x",
-    ((-157079632679)/(100000000000),
-    (157079632679)/(100000000000)))];
+    ((-157)/(100),
+    (157)/(100)))];
   |>
 End
 
diff --git a/testcases/timing/cert_ex2_8_sinScript.sml b/testcases/timing/cert_ex2_8_sinScript.sml
index 68cecd8f601bf073e2e7e8c5a2020551d3ea6d71..3f7d0ccb900c167a831671cf63d74fb65c6566c1 100644
--- a/testcases/timing/cert_ex2_8_sinScript.sml
+++ b/testcases/timing/cert_ex2_8_sinScript.sml
@@ -10,14 +10,14 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-1046841066988495)/(68719476736);
-    (570779987774089)/(137438953472);
-    (-7912644776784859)/(17592186044416);
-    (13617031604688847)/(562949953421312);
-    (-32298365546926466329580307501601055264472961425781)/(50000000000000000000000000000000000000000000000000);
-    (8567523582594961380036469034138235656428150832653)/(1250000000000000000000000000000000000000000000000000)
+    (-7797683)/(512);
+    (2125821)/(512);
+    (-3683767)/(8192);
+    (3169749)/(131072);
+    (-5417565)/(8388608);
+    (3678915)/(536870912)
     ];
-  eps := (1551109709473666616457336499137553924529463142711)/(400000000000000000000000000000000000000000000000) ;
+  eps := (38768960053030845104387898217880847967582490010993)/(10000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((17)/(1),
     (21)/(1)))];
diff --git a/testcases/timing/cert_ex2_9_cosScript.sml b/testcases/timing/cert_ex2_9_cosScript.sml
index e3db097c8576c75b842768da321c0cd157de339c..95bc006e34606f37f384eea3a4411f71be3bc30b 100644
--- a/testcases/timing/cert_ex2_9_cosScript.sml
+++ b/testcases/timing/cert_ex2_9_cosScript.sml
@@ -10,14 +10,14 @@ Definition cos_example_def:
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (49201749738733471795093521450326079502701759338379)/(50000000000000000000000000000000000000000000000000);
-    (43231317198734867113252278159052366390824317932129)/(1000000000000000000000000000000000000000000000000000);
-    (-26910809951929021144323428416100796312093734741211)/(50000000000000000000000000000000000000000000000000);
-    (10627689143904646938698643765519591397605836391449)/(2000000000000000000000000000000000000000000000000000);
-    (52831992368872076476504773268061398994177579879761)/(1000000000000000000000000000000000000000000000000000);
-    (-34621610831799922488455356628378467576112598180771)/(5000000000000000000000000000000000000000000000000000)
+    (1031835)/(1048576);
+    (2901293)/(67108864);
+    (-4514897)/(8388608);
+    (2853269)/(536870912);
+    (7090963)/(134217728);
+    (-7434913)/(1073741824)
     ];
-  eps := (1921637155239867126100469433357648601099225142823)/(62500000000000000000000000000000000000000000000000000) ;
+  eps := (15371553308635636074028096109354240926555707976171)/(500000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(1),
     (6283)/(2000)))];
diff --git a/testcases/timing/cert_ex2_9_sinScript.sml b/testcases/timing/cert_ex2_9_sinScript.sml
index af494ce25629d140a651146af6cd97b61cce8f63..f9848ed08a5c6a9bf134117a5c39e6b342bbc98d 100644
--- a/testcases/timing/cert_ex2_9_sinScript.sml
+++ b/testcases/timing/cert_ex2_9_sinScript.sml
@@ -10,14 +10,14 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (62920263623963731958177447722846409305930137634277)/(1000000000000000000000000000000000000000000000000000);
-    (78645180369122169583562254047137685120105743408203)/(100000000000000000000000000000000000000000000000000);
-    (5812402510609683270459413506614509969949722290039)/(20000000000000000000000000000000000000000000000000);
-    (-18418171095430309336382634910478373058140277862549)/(50000000000000000000000000000000000000000000000000);
-    (73679317500971966414802238887205021455883979797363)/(1000000000000000000000000000000000000000000000000000);
-    (-18909550722234630404372524026257451623678207397461)/(5000000000000000000000000000000000000000000000000000)
+    (4222517)/(67108864);
+    (412327)/(524288);
+    (2437903)/(8388608);
+    (-3090059)/(8388608);
+    (4944541)/(67108864);
+    (-8121609)/(2147483648)
     ];
-  eps := (27635690117192945775859077717383532873410368414153)/(500000000000000000000000000000000000000000000000000000) ;
+  eps := (13817531046447314259825955154435239665923136306389)/(250000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(1),
     (6283)/(2000)))];
diff --git a/testcases/timing/cert_ex3_c_expScript.sml b/testcases/timing/cert_ex3_c_expScript.sml
index 5bd02a6b24ba9a248437609702e7d3dcce6c4ee0..6382b2f6f2d263dc784c6b8613162a132979bd80 100644
--- a/testcases/timing/cert_ex3_c_expScript.sml
+++ b/testcases/timing/cert_ex3_c_expScript.sml
@@ -10,14 +10,14 @@ Definition exp_example_def:
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (4999994352151027332542554404426482506096363067627)/(5000000000000000000000000000000000000000000000000);
-    (25001986418547264556799802903697127476334571838379)/(25000000000000000000000000000000000000000000000000);
-    (9981921974344121761824055738543393090367317199707)/(20000000000000000000000000000000000000000000000000);
-    (10650123358232420345270696770967333577573299407959)/(62500000000000000000000000000000000000000000000000);
-    (3480057116490031451916387084111192962154746055603)/(100000000000000000000000000000000000000000000000000);
-    (69518640516647574149888821892773194122128188610077)/(5000000000000000000000000000000000000000000000000000)
+    (8388599)/(8388608);
+    (4194633)/(4194304);
+    (4186767)/(8388608);
+    (5717337)/(33554432);
+    (4672443)/(134217728);
+    (466389)/(33554432)
     ];
-  eps := (7178351457796307075602269310730310995538987355331)/(6250000000000000000000000000000000000000000000000000000) ;
+  eps := (11525108961713547379099310341720199971842524890871)/(10000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (1)/(1)))];
diff --git a/testcases/timing/cert_ex3_d_expScript.sml b/testcases/timing/cert_ex3_d_expScript.sml
index 75cf6152024b1ee72bbc6b9ee806364cdd0c1b20..a8e9063048975e5cf31dc58a0c87a80ef5aa5350 100644
--- a/testcases/timing/cert_ex3_d_expScript.sml
+++ b/testcases/timing/cert_ex3_d_expScript.sml
@@ -10,14 +10,14 @@ Definition exp_example_def:
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (-4104452836858037134692978042949107475578784942627)/(1250000000000000000000000000000000000000000000000);
-    (5548488435264213)/(140737488355328);
-    (-15433440591628771)/(281474976710656);
-    (15970972624344373)/(562949953421312);
-    (-14925107079181717528726380805892404168844223022461)/(2500000000000000000000000000000000000000000000000);
-    (48250575788324201464973839392769150435924530029297)/(100000000000000000000000000000000000000000000000000)
+    (-1721543)/(524288);
+    (5167443)/(131072);
+    (-3593383)/(65536);
+    (7437071)/(262144);
+    (-391253)/(65536);
+    (8095107)/(16777216)
     ];
-  eps := (55986189266726386229083272120231239854952043212957)/(10000000000000000000000000000000000000000000000000) ;
+  eps := (55986199515466994848038486229608542141384852360727)/(10000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (7)/(1)))];
diff --git a/testcases/timing/cert_ex3_d_sinScript.sml b/testcases/timing/cert_ex3_d_sinScript.sml
index fb10148f58f7397c8cc6776558169f04545d0630..a5bd367508181e4ce27a1a54d945addb0dc5378f 100644
--- a/testcases/timing/cert_ex3_d_sinScript.sml
+++ b/testcases/timing/cert_ex3_d_sinScript.sml
@@ -10,14 +10,14 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-24228462505845824517813902332363795721903443336487)/(1000000000000000000000000000000000000000000000000000);
-    (27352806221912512318894528107193764299154281616211)/(25000000000000000000000000000000000000000000000000);
-    (8200659384425642260685318518653730279766023159027)/(500000000000000000000000000000000000000000000000000);
-    (-3576105450507626945522154926493385573849081993103)/(12500000000000000000000000000000000000000000000000);
-    (1359773773486757930673007876976043917238712310791)/(20000000000000000000000000000000000000000000000000);
-    (-43385477306031078499615194488114866544492542743683)/(10000000000000000000000000000000000000000000000000000)
+    (-6503879)/(268435456);
+    (4589045)/(4194304);
+    (2201183)/(134217728);
+    (-299985)/(1048576);
+    (4562639)/(67108864);
+    (-1164619)/(268435456)
     ];
-  eps := (339327532675471526764518441329513998160221522019)/(10000000000000000000000000000000000000000000000000) ;
+  eps := (16966333881232128935700906020572419832983797903381)/(500000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (7)/(1)))];
diff --git a/testcases/timing/cert_forwardk2jX_cosScript.sml b/testcases/timing/cert_forwardk2jX_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..dc8214b447d6a2e906fff93641f4269678bdc55a
--- /dev/null
+++ b/testcases/timing/cert_forwardk2jX_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_forwardk2jX_cos";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "theta1");
+    poly := [
+    (2097169)/(2097152);
+    (-5285315)/(17179869184);
+    (-8349665)/(16777216);
+    (-1787835)/(268435456);
+    (3389287)/(67108864);
+    (-5970771)/(1073741824)
+    ];
+  eps := (10667810060499641756895072302472422990957022994561)/(2000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta1",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_forwardk2jY_sinScript.sml b/testcases/timing/cert_forwardk2jY_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..23a400cafa5f81deb53edff839a1316f1c1fa49e
--- /dev/null
+++ b/testcases/timing/cert_forwardk2jY_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_forwardk2jY_sin";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "theta1");
+    poly := [
+    (4118863)/(549755813888);
+    (4193183)/(4194304);
+    (4009913)/(2147483648);
+    (-2877369)/(16777216);
+    (5861875)/(1073741824);
+    (6346265)/(1073741824)
+    ];
+  eps := (50212791961457274158431077054229880298681030861107)/(10000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta1",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_hartman3_expScript.sml b/testcases/timing/cert_hartman3_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..d6f6f483f274f8a7067fec5547c87896d1fdd8ab
--- /dev/null
+++ b/testcases/timing/cert_hartman3_expScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_hartman3_exp";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "e1");
+    poly := [
+    (-4408348672)/(1);
+    (-2842592768)/(1);
+    (380896128)/(1);
+    (49098408)/(1);
+    (-6542058)/(1);
+    (5546545)/(32)
+    ];
+  eps := (17610116977916449163688205319658604320970200999071)/(2000000000000000000000000000000000000000) ;
+  iv := [("e1",
+    ((-760706967)/(100000000),
+    (2509723033)/(100000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_hartman6_expScript.sml b/testcases/timing/cert_hartman6_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..37ecb25cbf0f3fdf4db4fee27f92d165561873ce
--- /dev/null
+++ b/testcases/timing/cert_hartman6_expScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_hartman6_exp";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "e1");
+    poly := [
+    (-365101248)/(1);
+    (-107537088)/(1);
+    (30747656)/(1);
+    (6206029)/(4);
+    (-823633)/(2);
+    (7089153)/(512)
+    ];
+  eps := (46047460659598446320411616171840492178908641293161)/(100000000000000000000000000000000000000000) ;
+  iv := [("e1",
+    ((-7979168397)/(1000000000),
+    (22240841603)/(1000000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_instantaneousCurrent_cosScript.sml b/testcases/timing/cert_instantaneousCurrent_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..f94a885abcbd736e63102125216cb4a8401e80bf
--- /dev/null
+++ b/testcases/timing/cert_instantaneousCurrent_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_instantaneousCurrent_cos";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "_tmp4");
+    poly := [
+    (-3243245)/(2251799813685248);
+    (13360620661033439926512755846488289535045623779297)/(100000000000000000000000000000000000000000000000000000000000000);
+    (-9438085294296355353760655249040212311228970065713)/(2500000000000000000000000000000000000000000000000000000000000000000);
+    (11186727634134247912914575965733182498496045553793)/(250000000000000000000000000000000000000000000000000000000000000000000000);
+    (-2347503490668963264256886650360141106538521601349)/(10000000000000000000000000000000000000000000000000000000000000000000000000000);
+    (4503163656011676437880693176852493067098658252307)/(10000000000000000000000000000000000000000000000000000000000000000000000000000000000)
+    ];
+  eps := (2000000002880999970172337895089616881824366623697)/(2000000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp4",
+    ((-7074178169367831)/(4503599627370496),
+    (17802902220171114143381873073366743)/(94447329657392904273920000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_integrate18257_cosScript.sml b/testcases/timing/cert_integrate18257_cosScript.sml
index 3019a19a9843860a866049544e80e486965bb741..c985bb60542486cdcfa4abd8c14c6122e17240b7 100644
--- a/testcases/timing/cert_integrate18257_cosScript.sml
+++ b/testcases/timing/cert_integrate18257_cosScript.sml
@@ -10,14 +10,14 @@ Definition cos_example_def:
   <|
     transc := Fun Cos (Var "x");
     poly := [
-    (50003385320083115761491399098304100334644317626953)/(50000000000000000000000000000000000000000000000000);
-    (-52279045960208721027448475204835176555206999182701)/(25000000000000000000000000000000000000000000000000000);
-    (-24473746053163661362539471610944019630551338195801)/(50000000000000000000000000000000000000000000000000);
-    (-19736745776220787282340118906631687423214316368103)/(1000000000000000000000000000000000000000000000000000);
-    (14754445077735818363240394290869517135433852672577)/(250000000000000000000000000000000000000000000000000);
-    (-37571885860189662732777637899062028736807405948639)/(5000000000000000000000000000000000000000000000000000)
+    (1048647)/(1048576);
+    (-1122699)/(536870912);
+    (-8212025)/(16777216);
+    (-2649033)/(134217728);
+    (7921237)/(134217728);
+    (-4034253)/(536870912)
     ];
-  eps := (5108359546927102172713305009190372907884584447487)/(40000000000000000000000000000000000000000000000000000) ;
+  eps := (25541412445303020488732747776187920526854870591353)/(200000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (157)/(50)))];
diff --git a/testcases/timing/cert_integrate18257_expScript.sml b/testcases/timing/cert_integrate18257_expScript.sml
index 64daa1f4889c00c2d75261307ec72d227dbfa719..aa1ac9f3bdb526917e4e6fd782d030e539976e87 100644
--- a/testcases/timing/cert_integrate18257_expScript.sml
+++ b/testcases/timing/cert_integrate18257_expScript.sml
@@ -10,14 +10,14 @@ Definition exp_example_def:
   <|
     transc := Fun Exp (Var "_tmp6");
     poly := [
-    (5000223750638280173497207670152420178055763244629)/(5000000000000000000000000000000000000000000000000);
-    (1125943082178271)/(1125899906842624);
-    (49919698464568396101270764120272360742092132568359)/(100000000000000000000000000000000000000000000000000);
-    (166424651222845970677255422742746304720640182495117)/(1000000000000000000000000000000000000000000000000000);
-    (342138231961014980826024656224149111949373036623)/(7812500000000000000000000000000000000000000000000);
-    (17476392011412390445346254352898540673777461051941)/(2000000000000000000000000000000000000000000000000000)
+    (1048623)/(1048576);
+    (4194465)/(4194304);
+    (8375131)/(16777216);
+    (5584281)/(33554432);
+    (5877919)/(134217728);
+    (2345661)/(268435456)
     ];
-  eps := (45276585756192300003908221673909677955123689591867)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (22654591998493733409533957795670142933031106425969)/(500000000000000000000000000000000000000000000000000000) ;
   iv := [("_tmp6",
     ((-1125898478894779)/(1125899906842624),
     (1)/(1)))];
diff --git a/testcases/timing/cert_integrate18257_sinScript.sml b/testcases/timing/cert_integrate18257_sinScript.sml
index 6293289fc714449d62a89e2918bd47e98070c9e4..b291eedc78d02f3e021d7772efebdf55174ed1d3 100644
--- a/testcases/timing/cert_integrate18257_sinScript.sml
+++ b/testcases/timing/cert_integrate18257_sinScript.sml
@@ -10,14 +10,14 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (14875275141961862707118413595708261709660291671753)/(25000000000000000000000000000000000000000000000000000);
-    (98656012188654773620299920366960577666759490966797)/(100000000000000000000000000000000000000000000000000);
-    (48998607825437131418899738832806178834289312362671)/(1000000000000000000000000000000000000000000000000000);
-    (-231067427833732755293461025303258793428540229797363)/(1000000000000000000000000000000000000000000000000000);
-    (9187517832290102368086870399110921425744891166687)/(250000000000000000000000000000000000000000000000000);
-    (29478188028054012618026221911882167603380366927013)/(5000000000000000000000000000000000000000000000000000000)
+    (5111123)/(8589934592);
+    (4137933)/(4194304);
+    (822061)/(16777216);
+    (-3876669)/(16777216);
+    (2466257)/(67108864);
+    (1619721)/(274877906944)
     ];
-  eps := (727234297766965309799844276264620800663697400909)/(625000000000000000000000000000000000000000000000000) ;
+  eps := (11635750012739223885040680429836601410629114564153)/(10000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((0)/(1),
     (157)/(50)))];
diff --git a/testcases/timing/cert_integrateStoutemyer2007_expScript.sml b/testcases/timing/cert_integrateStoutemyer2007_expScript.sml
index 3032c1da72b6ede1de58d0bdd5c2d75bd37bd13a..d9ba759e8070f60bbfdad2bda9ab9840c8256c4a 100644
--- a/testcases/timing/cert_integrateStoutemyer2007_expScript.sml
+++ b/testcases/timing/cert_integrateStoutemyer2007_expScript.sml
@@ -10,14 +10,14 @@ Definition exp_example_def:
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (4999923290900973593675615802567335776984691619873)/(5000000000000000000000000000000000000000000000000);
-    (563111624041217)/(562949953421312);
-    (49810037635939313771515912776521872729063034057617)/(100000000000000000000000000000000000000000000000000);
-    (17247714617256310054571599721384700387716293334961)/(100000000000000000000000000000000000000000000000000);
-    (32848213104541060941565788766638434026390314102173)/(1000000000000000000000000000000000000000000000000000);
-    (14583620073919503594417346192813056404702365398407)/(1000000000000000000000000000000000000000000000000000)
+    (8388479)/(8388608);
+    (4195511)/(4194304);
+    (8356687)/(16777216);
+    (2893797)/(16777216);
+    (4407951)/(134217728);
+    (7830751)/(536870912)
     ];
-  eps := (16133005043482216797675644309777256702129399943703)/(25000000000000000000000000000000000000000000000000000000) ;
+  eps := (6432237487500849104472852963317165366565931549287)/(10000000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(10),
     (1)/(1)))];
diff --git a/testcases/timing/cert_integrateStoutemyer2007_logScript.sml b/testcases/timing/cert_integrateStoutemyer2007_logScript.sml
index b537ecee12a1f8d2a17f5ed34dbe34f55ac38def..25f74e3187e843a1954c49820a5e76adb925cb20 100644
--- a/testcases/timing/cert_integrateStoutemyer2007_logScript.sml
+++ b/testcases/timing/cert_integrateStoutemyer2007_logScript.sml
@@ -10,14 +10,14 @@ Definition log_example_def:
   <|
     transc := Fun Log (Var "_tmp12");
     poly := [
-    (-1003727418270451629545014782252110308036208152771)/(625000000000000000000000000000000000000000000000);
-    (1419979547527991)/(562949953421312);
-    (-125519624523831963003317468974273651838302612304687)/(100000000000000000000000000000000000000000000000000);
-    (41081633581412535516363959686714224517345428466797)/(100000000000000000000000000000000000000000000000000);
-    (-3731904761401391712460906546766636893153190612793)/(50000000000000000000000000000000000000000000000000);
-    (892499419482766875953011487254684652725700289011)/(156250000000000000000000000000000000000000000000000)
+    (-1683989)/(1048576);
+    (1322477)/(524288);
+    (-2632411)/(2097152);
+    (6892651)/(16777216);
+    (-5009171)/(67108864);
+    (6133665)/(1073741824)
     ];
-  eps := (12495255185049274020460750480302127519133052571341)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (156277693095629183961857800607749254679448829433)/(12500000000000000000000000000000000000000000000000000) ;
   iv := [("_tmp12",
     ((6164586730295981)/(4503599627370496),
     (12876425955923819)/(4503599627370496)))];
diff --git a/testcases/timing/cert_integrateStoutemyer2007_sqrtScript.sml b/testcases/timing/cert_integrateStoutemyer2007_sqrtScript.sml
index 59eb766d09d3252c4afff60f144aa432c02319fc..00285d5882b761bc5ff45195d9af6f27fe5ac875 100644
--- a/testcases/timing/cert_integrateStoutemyer2007_sqrtScript.sml
+++ b/testcases/timing/cert_integrateStoutemyer2007_sqrtScript.sml
@@ -10,14 +10,14 @@ Definition sqrt_example_def:
   <|
     transc := Fun Sqrt (Var "x");
     poly := [
-    (137368231669103113556928974503534846007823944091797)/(1000000000000000000000000000000000000000000000000000);
-    (2391312353193661)/(1125899906842624);
-    (-9489667507569133908518210773763712495565414428711)/(2500000000000000000000000000000000000000000000000);
-    (26959973064441737911067775712581351399421691894531)/(5000000000000000000000000000000000000000000000000);
-    (-289435195526731)/(70368744177664);
-    (31406997206676795508784039157035294920206069946289)/(25000000000000000000000000000000000000000000000000)
+    (144041)/(1048576);
+    (4454167)/(2097152);
+    (-7960513)/(2097152);
+    (5653919)/(1048576);
+    (-4312923)/(1048576);
+    (5269223)/(4194304)
     ];
-  eps := (101691034404149997778409366615966000437107062409357)/(100000000000000000000000000000000000000000000000000000) ;
+  eps := (101691150348021015432078806429149853565536579103087)/(100000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((1)/(10),
     (1)/(1)))];
diff --git a/testcases/timing/cert_logTwo_logScript.sml b/testcases/timing/cert_logTwo_logScript.sml
index 96db37bcb7a7e8c44548d43a480ca14c719a1de4..2d37ce33cd936b5d08a9b608202d48dcd59effdf 100644
--- a/testcases/timing/cert_logTwo_logScript.sml
+++ b/testcases/timing/cert_logTwo_logScript.sml
@@ -10,14 +10,14 @@ Definition log_example_def:
   <|
     transc := Fun Log (Var "x");
     poly := [
-    (858313732018035)/(562949953421312);
-    (110290780955278014396903074612055206671357154846191)/(1000000000000000000000000000000000000000000000000000);
-    (-1502210755130700643245403314018915352789917960763)/(625000000000000000000000000000000000000000000000000);
-    (34503972293196385947439130958969144558068364858627)/(1000000000000000000000000000000000000000000000000000000);
-    (-13768193433739089191068018800181982363994848128641)/(50000000000000000000000000000000000000000000000000000000);
-    (46348596017119103882095291059659697419093049575167)/(50000000000000000000000000000000000000000000000000000000000)
+    (6394907)/(4194304);
+    (7401543)/(67108864);
+    (-5161637)/(2147483648);
+    (4742307)/(137438953472);
+    (-4844421)/(17592186044416);
+    (8349803)/(9007199254740992)
     ];
-  eps := (8700026535981789808957523077401995224851351825911)/(1000000000000000000000000000000000000000000000000000000) ;
+  eps := (2718335609361460400900244223107068057422952969137)/(312500000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((32)/(1),
     (64)/(1)))];
diff --git a/testcases/timing/cert_logexp_expScript.sml b/testcases/timing/cert_logexp_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..0cf0171482b19aa74231b35995fe8552aff0e1f4
--- /dev/null
+++ b/testcases/timing/cert_logexp_expScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_logexp_exp";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "x");
+    poly := [
+    (146175)/(2048);
+    (7892877)/(131072);
+    (-2213209)/(131072);
+    (-5119667)/(1048576);
+    (4896217)/(8388608);
+    (3592779)/(33554432)
+    ];
+  eps := (111827431699473981992795001936895113806900717911853)/(1000000000000000000000000000000000000000000000000) ;
+  iv := [("x",
+    ((-8)/(1),
+    (8)/(1)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_logexp_logScript.sml b/testcases/timing/cert_logexp_logScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..edccb119f4ae29c2ef41d5ab8476c653a62e8a6d
--- /dev/null
+++ b/testcases/timing/cert_logexp_logScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_logexp_log";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition log_example_def:
+  log_example =
+  <|
+    transc := Fun Log (Var "e");
+    poly := [
+    (-7005737)/(2097152);
+    (6768687)/(67108864);
+    (-8337483)/(34359738368);
+    (3845119)/(17592186044416);
+    (-1476151)/(18014398509481984);
+    (27107739406580406982261166604075697250664234161377)/(2500000000000000000000000000000000000000000000000000000000000000)
+    ];
+  eps := (48660259584777380061432006976848288976372221521017)/(10000000000000000000000000000000000000000000000000) ;
+  iv := [("e",
+    ((1547048310802923)/(4611686018427387904),
+    (6555195937328239)/(2199023255552)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert log_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_pendulum1_sinScript.sml b/testcases/timing/cert_pendulum1_sinScript.sml
index 750ef265f24776e1316862f6326b162be7a5bb32..0afe8b55772cd910cca925b5c45f5de32ffbe377 100644
--- a/testcases/timing/cert_pendulum1_sinScript.sml
+++ b/testcases/timing/cert_pendulum1_sinScript.sml
@@ -10,17 +10,17 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "t");
     poly := [
-    (-4120878125953392131611661277767914640050156416251)/(250000000000000000000000000000000000000000000000000000000000);
-    (9987651300427277667459691201656823977828025817871)/(10000000000000000000000000000000000000000000000000);
-    (681078440888968438406926152279218487917145097299)/(8000000000000000000000000000000000000000000000000000000000);
-    (-1025961551446071158555373159515511360950767993927)/(6250000000000000000000000000000000000000000000000);
-    (-20566524970202187191946860666612019669444166858341)/(500000000000000000000000000000000000000000000000000000000000);
-    (7042122231715413401692549300037171633448451757431)/(1000000000000000000000000000000000000000000000000000)
+    (6239177)/(549755813888);
+    (8385379)/(8388608);
+    (5438371)/(2147483648);
+    (-362461)/(2097152);
+    (7023561)/(1073741824);
+    (6017645)/(1073741824)
     ];
-  eps := (35012358135519999186113430790368047983907472943059)/(100000000000000000000000000000000000000000000000000000) ;
+  eps := (38841047918052682415603348695925551222672236589557)/(5000000000000000000000000000000000000000000000000000000) ;
   iv := [("t",
-    ((-2)/(1),
-    (2)/(1)))];
+    ((1)/(100),
+    (8)/(5)))];
   |>
 End
 
diff --git a/testcases/timing/cert_pendulum2_cosScript.sml b/testcases/timing/cert_pendulum2_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..7374c801576960ee67a40aeb97d1742e735e43e7
--- /dev/null
+++ b/testcases/timing/cert_pendulum2_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_pendulum2_cos";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "w");
+    poly := [
+    (1418701)/(2097152);
+    (6893901)/(8388608);
+    (-2684765)/(2097152);
+    (2851387)/(8388608);
+    (-1284003)/(67108864);
+    (-8329267)/(8589934592)
+    ];
+  eps := (21599085658042602699163830706895449118480811568467)/(5000000000000000000000000000000000000000000000000000) ;
+  iv := [("w",
+    ((1)/(1),
+    (5)/(1)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_pendulum2_expScript.sml b/testcases/timing/cert_pendulum2_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..15663252f4ae88da935c6d667ac683897351f6ac
--- /dev/null
+++ b/testcases/timing/cert_pendulum2_expScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_pendulum2_exp";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "_tmp31");
+    poly := [
+    (4683421)/(2097152);
+    (4298581)/(2097152);
+    (-6160169)/(16777216);
+    (-6091005)/(67108864);
+    (4205677)/(33554432);
+    (3220747)/(134217728)
+    ];
+  eps := (2013873268271239767737859518464628171240905395299)/(1250000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp31",
+    ((-196133)/(40000),
+    (196133)/(40000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_pendulum2_sinScript.sml b/testcases/timing/cert_pendulum2_sinScript.sml
index 1ceff974ec2cc47f5caef105366d29818aa451a6..d951e285de1ec71e026616e7a5bd6051e5b7e38b 100644
--- a/testcases/timing/cert_pendulum2_sinScript.sml
+++ b/testcases/timing/cert_pendulum2_sinScript.sml
@@ -8,19 +8,19 @@ val _ = realZeroLib.useBinary := false;
 Definition sin_example_def:
   sin_example =
   <|
-    transc := Fun Sin (Var "t");
+    transc := Fun Sin (Var "_tmp20");
     poly := [
-    (-4120878125953392131611661277767914640050156416251)/(250000000000000000000000000000000000000000000000000000000000);
-    (9987651300427277667459691201656823977828025817871)/(10000000000000000000000000000000000000000000000000);
-    (681078440888968438406926152279218487917145097299)/(8000000000000000000000000000000000000000000000000000000000);
-    (-1025961551446071158555373159515511360950767993927)/(6250000000000000000000000000000000000000000000000);
-    (-20566524970202187191946860666612019669444166858341)/(500000000000000000000000000000000000000000000000000000000000);
-    (7042122231715413401692549300037171633448451757431)/(1000000000000000000000000000000000000000000000000000)
+    (3474249)/(274877906944);
+    (8385717)/(8388608);
+    (2360121)/(1073741824);
+    (-5773919)/(33554432);
+    (6320141)/(1073741824);
+    (3111643)/(536870912)
     ];
-  eps := (35012358135519999186113430790368047983907472943059)/(100000000000000000000000000000000000000000000000000000) ;
-  iv := [("t",
-    ((-2)/(1),
-    (2)/(1)))];
+  eps := (2133300829949805468708062732356179485646514316271)/(400000000000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp20",
+    ((1)/(40),
+    (61)/(40)))];
   |>
 End
 
diff --git a/testcases/timing/cert_polarToCarthesian_x_cosScript.sml b/testcases/timing/cert_polarToCarthesian_x_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..d05ee271157f78bbdb87cd39ee6424b8a9d60ea7
--- /dev/null
+++ b/testcases/timing/cert_polarToCarthesian_x_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_polarToCarthesian_x_cos";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "radiant");
+    poly := [
+    (1018001)/(1048576);
+    (2628809)/(8388608);
+    (-1086653)/(1048576);
+    (1316981)/(4194304);
+    (-52401)/(2097152);
+    (-4527969)/(9007199254740992)
+    ];
+  eps := (33554955984331639857364301917945721368339235299117)/(1000000000000000000000000000000000000000000000000000) ;
+  iv := [("radiant",
+    ((0)/(1),
+    (314159265359)/(50000000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_polarToCarthesian_y_sinScript.sml b/testcases/timing/cert_polarToCarthesian_y_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..5995ab1faef7a75ff17be905f62ca37268d1f9c4
--- /dev/null
+++ b/testcases/timing/cert_polarToCarthesian_y_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_polarToCarthesian_y_sin";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "radiant");
+    poly := [
+    (7355129)/(1073741824);
+    (7529033)/(8388608);
+    (8330443)/(33554432);
+    (-6475181)/(16777216);
+    (5761317)/(67108864);
+    (-5868429)/(1073741824)
+    ];
+  eps := (6339304632133464058442752382745542945831689462461)/(500000000000000000000000000000000000000000000000000) ;
+  iv := [("radiant",
+    ((0)/(1),
+    (314159265359)/(50000000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_predictGaussianNB_logScript.sml b/testcases/timing/cert_predictGaussianNB_logScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..cbdc154e7fdbf3f5b1492ab7410ef3c99b7e344a
--- /dev/null
+++ b/testcases/timing/cert_predictGaussianNB_logScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_predictGaussianNB_log";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition log_example_def:
+  log_example =
+  <|
+    transc := Fun Log (Var "_tmp");
+    poly := [
+    (-8292145)/(4194304);
+    (7576055)/(2097152);
+    (-5274527)/(2097152);
+    (4723819)/(4194304);
+    (-1150253)/(4194304);
+    (3705825)/(134217728)
+    ];
+  eps := (5541900224522055798539880566309859925505411170743)/(25000000000000000000000000000000000000000000000000000) ;
+  iv := [("_tmp",
+    ((9423)/(12500),
+    (3141)/(1250)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert log_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_predictMLPLogistic_expScript.sml b/testcases/timing/cert_predictMLPLogistic_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..1accdb8a15fdff29b66ed22b17b6b6af90434ed1
--- /dev/null
+++ b/testcases/timing/cert_predictMLPLogistic_expScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_predictMLPLogistic_exp";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "n1");
+    poly := [
+    (258843)/(131072);
+    (5287075)/(8388608);
+    (-5427323)/(33554432);
+    (7080553)/(33554432);
+    (1845357)/(16777216);
+    (6219349)/(536870912)
+    ];
+  eps := (54153550745832152346572980644604392591546598729427)/(50000000000000000000000000000000000000000000000000) ;
+  iv := [("n1",
+    ((-121)/(20),
+    (87)/(20)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_rodriguesRotation_cosScript.sml b/testcases/timing/cert_rodriguesRotation_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..9eda4c6f56bcb5236becd1d39a6162e751725b5e
--- /dev/null
+++ b/testcases/timing/cert_rodriguesRotation_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_rodriguesRotation_cos";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "theta");
+    poly := [
+    (4194327)/(4194304);
+    (-2346973)/(8589934592);
+    (-4175907)/(8388608);
+    (-3470883)/(536870912);
+    (1690273)/(33554432);
+    (-2968411)/(536870912)
+    ];
+  eps := (55771079097846253630718383277312210929156777720063)/(10000000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta",
+    ((0)/(1),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_rodriguesRotation_sinScript.sml b/testcases/timing/cert_rodriguesRotation_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..6d2ecbfb7ea09812aa3d591e50cd301d2dd268e0
--- /dev/null
+++ b/testcases/timing/cert_rodriguesRotation_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_rodriguesRotation_sin";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "theta");
+    poly := [
+    (5692011)/(1099511627776);
+    (4193307)/(4194304);
+    (7556803)/(4294967296);
+    (-2874655)/(16777216);
+    (1436837)/(268435456);
+    (3186899)/(536870912)
+    ];
+  eps := (6497336012837779230942629400952705423393633904231)/(1250000000000000000000000000000000000000000000000000000) ;
+  iv := [("theta",
+    ((0)/(1),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_sine_sinScript.sml b/testcases/timing/cert_sine_sinScript.sml
index 2e0a03f587d4c9b38c680d1d233166ffd1694dea..548d6243e7f3d33ff92166056eb380346dfdc7ec 100644
--- a/testcases/timing/cert_sine_sinScript.sml
+++ b/testcases/timing/cert_sine_sinScript.sml
@@ -10,14 +10,14 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x");
     poly := [
-    (-27761522985246471972987058430257085420329865588229)/(10000000000000000000000000000000000000000000000000000000000000);
-    (99969677314052479699668651846877764910459518432617)/(100000000000000000000000000000000000000000000000000);
-    (11536456095163883772080219177679652020444833748769)/(500000000000000000000000000000000000000000000000000000000000);
-    (-165673079310543952535894618449674453586339950561523)/(1000000000000000000000000000000000000000000000000000);
-    (-179764345886510341357370401589800990461293084266003)/(10000000000000000000000000000000000000000000000000000000000000);
-    (75143771680937715765069562223743560025468468666077)/(10000000000000000000000000000000000000000000000000000)
+    (-3198861)/(1152921504606846976);
+    (524129)/(524288);
+    (3324061)/(144115188075855872);
+    (-694883)/(4194304);
+    (-2590085)/(144115188075855872);
+    (63035)/(8388608)
     ];
-  eps := (16948642788220920879930931195679997582486139089333)/(250000000000000000000000000000000000000000000000000000) ;
+  eps := (33894703867810707071243737666471249560151636361809)/(500000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-157079632679)/(100000000000),
     (157079632679)/(100000000000)))];
diff --git a/testcases/timing/cert_sinxx10_sinScript.sml b/testcases/timing/cert_sinxx10_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..5ebf3600d1b03529efc35e06c5945855c58cf0b8
--- /dev/null
+++ b/testcases/timing/cert_sinxx10_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_sinxx10_sin";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "x");
+    poly := [
+    (4118863)/(549755813888);
+    (4193183)/(4194304);
+    (4009913)/(2147483648);
+    (-2877369)/(16777216);
+    (5861875)/(1073741824);
+    (6346265)/(1073741824)
+    ];
+  eps := (50212791961457274158431077054229880298681030861107)/(10000000000000000000000000000000000000000000000000000000) ;
+  iv := [("x",
+    ((1)/(100),
+    (3)/(2)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_sphere_cosScript.sml b/testcases/timing/cert_sphere_cosScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..5849e718c07fa4d26f071ff7666230c28f05ec63
--- /dev/null
+++ b/testcases/timing/cert_sphere_cosScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_sphere_cos";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition cos_example_def:
+  cos_example =
+  <|
+    transc := Fun Cos (Var "lon");
+    poly := [
+    (1018001)/(1048576);
+    (6368239)/(36028797018963968);
+    (-1859515)/(4194304);
+    (-6836407)/(144115188075855872);
+    (6707329)/(268435456);
+    (6898687)/(2305843009213693952)
+    ];
+  eps := (30240780132629784986275483638710557200165187553409)/(1000000000000000000000000000000000000000000000000000) ;
+  iv := [("lon",
+    ((-62831853)/(20000000),
+    (62831853)/(20000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert cos_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_sphere_sinScript.sml b/testcases/timing/cert_sphere_sinScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..8642c3c3a0ad02f63c7ccfd24e8f2317668ce77c
--- /dev/null
+++ b/testcases/timing/cert_sphere_sinScript.sml
@@ -0,0 +1,30 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_sphere_sin";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition sin_example_def:
+  sin_example =
+  <|
+    transc := Fun Sin (Var "lat");
+    poly := [
+    (-100005)/(36028797018963968);
+    (524129)/(524288);
+    (6649505)/(288230376151711744);
+    (-694883)/(4194304);
+    (-1295199)/(72057594037927936);
+    (8068481)/(1073741824)
+    ];
+  eps := (16946036090739573298993305869163662136694606843177)/(250000000000000000000000000000000000000000000000000000) ;
+  iv := [("lat",
+    ((-392699)/(250000),
+    (392699)/(250000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert sin_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_stoutemyerEq2007_atanScript.sml b/testcases/timing/cert_stoutemyerEq2007_atanScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..06154bcd96910555feb6319bac9ee17f7e59c92f
--- /dev/null
+++ b/testcases/timing/cert_stoutemyerEq2007_atanScript.sml
@@ -0,0 +1,29 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_stoutemyerEq2007_atan";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition atan_example_def:
+  atan_example =
+  <|
+    transc := Fun Atn (Var "x");
+    poly := [
+    (-5280018032749440310613303164306824587713680537737)/(1250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000);
+    (1)/(1);
+    (46464163697311792167587571306939825833276502820013)/(100000000000000000000000000000000000000000000000000000000000000000000000000);
+    (-5592405)/(16777216);
+    (-5563509)/(1125899906842624)
+    ];
+  eps := (3051757812500000000000000000002459310385218894959)/(625000000000000000000000000000000000000000000000000000000000) ;
+  iv := [("x",
+    ((-1)/(100000000),
+    (1)/(100000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert atan_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_stoutemyerEq2007_expScript.sml b/testcases/timing/cert_stoutemyerEq2007_expScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..6a45a0c1cbc3820d78e61604305b07ae76a40c8e
--- /dev/null
+++ b/testcases/timing/cert_stoutemyerEq2007_expScript.sml
@@ -0,0 +1,29 @@
+
+open realZeroLib preambleDandelion;
+
+val _ = new_theory "cert_stoutemyerEq2007_exp";
+
+val _ = realZeroLib.useBinary := false;
+
+Definition exp_example_def:
+  exp_example =
+  <|
+    transc := Fun Exp (Var "x");
+    poly := [
+    (1)/(1);
+    (1)/(1);
+    (1)/(2);
+    (5592405)/(33554432);
+    (5592441)/(134217728)
+    ];
+  eps := (119209289550926769147946978252291317422770980284103)/(10000000000000000000000000000000000000000000000000000000000000000000000000) ;
+  iv := [("x",
+    ((-1)/(100000000),
+    (1)/(100000000)))];
+  |>
+End
+
+Theorem checkerSucceeds = validateCert exp_example_def ``32:num``;
+
+val _ = export_theory();
+      
\ No newline at end of file
diff --git a/testcases/timing/cert_tangent_tanScript.sml b/testcases/timing/cert_tangent_tanScript.sml
index 4de587ae3e7a98b0a57d532d134bcad0be06bf9b..e173174cce0854603854d6a4f3aa0d625ccb4036 100644
--- a/testcases/timing/cert_tangent_tanScript.sml
+++ b/testcases/timing/cert_tangent_tanScript.sml
@@ -10,14 +10,14 @@ Definition tan_example_def:
   <|
     transc := Fun Tan (Var "x");
     poly := [
-    (-29883137743315596468463013479777146130800247192383)/(100000000000000000000000000000000000000000000000000);
-    (2662617322598943)/(8192);
-    (3530466253083741068330425605381606146693229675293)/(2500000000000000000000000000000000000000000000000);
-    (-2158240620850177)/(4096);
-    (-13081305552817802662080026721014291979372501373291)/(25000000000000000000000000000000000000000000000000);
-    (5598103836226007)/(32768)
+    (-2506779)/(8388608);
+    (325026709504)/(1);
+    (5923141)/(4194304);
+    (-526914486272)/(1);
+    (-4389359)/(8388608);
+    (170840653824)/(1)
     ];
-  eps := (1029323694855253858755221323496773372999532437921)/(10000000000000000000000000000000000000) ;
+  eps := (51466175178566608806904464658023366963707842789519)/(500000000000000000000000000000000000000) ;
   iv := [("x",
     ((-157079632679)/(100000000000),
     (157079632679)/(100000000000)))];
diff --git a/testcases/timing/cert_testDepth1_expScript.sml b/testcases/timing/cert_testDepth1_expScript.sml
index b6577ffc32999e7ff6b31de4ed3a9fb403eed844..3419961af616b928be9dddf4b599e9e495d810be 100644
--- a/testcases/timing/cert_testDepth1_expScript.sml
+++ b/testcases/timing/cert_testDepth1_expScript.sml
@@ -10,14 +10,14 @@ Definition exp_example_def:
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (99987915063731530596058405535586643964052200317383)/(100000000000000000000000000000000000000000000000000);
-    (4984365670801103875842130719320266507565975189209)/(5000000000000000000000000000000000000000000000000);
-    (24339938129316959769532502377842320129275321960449)/(50000000000000000000000000000000000000000000000000);
-    (72895455004674286625387935600883793085813522338867)/(500000000000000000000000000000000000000000000000000);
-    (129509809668332852641836616669479553820565342903137)/(5000000000000000000000000000000000000000000000000000);
-    (41356933234823639068677980645816205651499330997467)/(20000000000000000000000000000000000000000000000000000)
+    (4193797)/(4194304);
+    (1045297)/(1048576);
+    (510445)/(1048576);
+    (4891919)/(33554432);
+    (3476487)/(134217728);
+    (4440639)/(2147483648)
     ];
-  eps := (6045557641546432382160815254578755256565772452217)/(50000000000000000000000000000000000000000000000000000) ;
+  eps := (12091150731540099862223415557632403947696541975831)/(100000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-3)/(1),
     (0)/(1)))];
diff --git a/testcases/timing/cert_testDepth2_expScript.sml b/testcases/timing/cert_testDepth2_expScript.sml
index ed46e1994509883ff8888bce7e0db32db9f37b1d..f19f16ed6993382aea962c8e591ef28b59c1ae24 100644
--- a/testcases/timing/cert_testDepth2_expScript.sml
+++ b/testcases/timing/cert_testDepth2_expScript.sml
@@ -10,14 +10,14 @@ Definition exp_example_def:
   <|
     transc := Fun Exp (Var "x");
     poly := [
-    (99987915063731530596058405535586643964052200317383)/(100000000000000000000000000000000000000000000000000);
-    (4984365670801103875842130719320266507565975189209)/(5000000000000000000000000000000000000000000000000);
-    (24339938129316959769532502377842320129275321960449)/(50000000000000000000000000000000000000000000000000);
-    (72895455004674286625387935600883793085813522338867)/(500000000000000000000000000000000000000000000000000);
-    (129509809668332852641836616669479553820565342903137)/(5000000000000000000000000000000000000000000000000000);
-    (41356933234823639068677980645816205651499330997467)/(20000000000000000000000000000000000000000000000000000)
+    (4193797)/(4194304);
+    (1045297)/(1048576);
+    (510445)/(1048576);
+    (4891919)/(33554432);
+    (3476487)/(134217728);
+    (4440639)/(2147483648)
     ];
-  eps := (6045557641546432382160815254578755256565772452217)/(50000000000000000000000000000000000000000000000000000) ;
+  eps := (12091150731540099862223415557632403947696541975831)/(100000000000000000000000000000000000000000000000000000) ;
   iv := [("x",
     ((-3)/(1),
     (0)/(1)))];
diff --git a/testcases/timing/cert_xu1_cosScript.sml b/testcases/timing/cert_xu1_cosScript.sml
index 6e42e7331ac5cf49e63c3434be47001aa0fde76d..22efe6b381e427de7bbfe1e8a18bd67de61bbf46 100644
--- a/testcases/timing/cert_xu1_cosScript.sml
+++ b/testcases/timing/cert_xu1_cosScript.sml
@@ -10,17 +10,17 @@ Definition cos_example_def:
   <|
     transc := Fun Cos (Var "x1");
     poly := [
-    (97091928396572901860395177209284156560897827148437)/(100000000000000000000000000000000000000000000000000);
-    (88102801838149783110816523083508094646432162733163)/(500000000000000000000000000000000000000000000000000000000000);
-    (-124817476790713)/(281474976710656);
-    (-47340982058707618492410287079998933157387597248089)/(1000000000000000000000000000000000000000000000000000000000000);
-    (125000945627423811282175059034216246800497174263)/(5000000000000000000000000000000000000000000000000);
-    (14944574916626695440490972902893799384438366928407)/(5000000000000000000000000000000000000000000000000000000000000)
+    (4194305)/(4194304);
+    (-7726885)/(549755813888);
+    (-4192685)/(8388608);
+    (-1118269)/(1073741824);
+    (5943217)/(134217728);
+    (-6610829)/(2147483648)
     ];
-  eps := (60325149764354696387657436231227704193819721325461)/(2000000000000000000000000000000000000000000000000000) ;
+  eps := (21521108370310592166099983098907383708740522513003)/(200000000000000000000000000000000000000000000000000000000) ;
   iv := [("x1",
-    ((-157)/(50),
-    (157)/(50)))];
+    ((1)/(100),
+    (3)/(4)))];
   |>
 End
 
diff --git a/testcases/timing/cert_xu1_sinScript.sml b/testcases/timing/cert_xu1_sinScript.sml
index 1b227a2e632835e00503d9c0b74aa4aca20f6a51..9f2fa6f9930430958dec6aead0b14032afc4618b 100644
--- a/testcases/timing/cert_xu1_sinScript.sml
+++ b/testcases/timing/cert_xu1_sinScript.sml
@@ -10,17 +10,17 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x1");
     poly := [
-    (-3458420040541902157599986648920916201821462721)/(6250000000000000000000000000000000000000000000000000000);
-    (9844584217973025852543855762633029371500015258789)/(10000000000000000000000000000000000000000000000000);
-    (11948551839482203120988263353690998769263131862317)/(10000000000000000000000000000000000000000000000000000000000);
-    (-153486018610747773638358637526835082098841667175293)/(1000000000000000000000000000000000000000000000000000);
-    (-5981023209126048755582390573250608015176688070369)/(25000000000000000000000000000000000000000000000000000000000);
-    (13669493890370461829097958883494356996379792690277)/(2500000000000000000000000000000000000000000000000000)
+    (184799)/(2199023255552);
+    (4194283)/(4194304);
+    (4557931)/(68719476736);
+    (-5603619)/(33554432);
+    (6348757)/(8589934592);
+    (258023)/(33554432)
     ];
-  eps := (1020940859788826944075336902524496760092532056821)/(125000000000000000000000000000000000000000000000000) ;
+  eps := (4431294656700195635751428473525062443002787342393)/(100000000000000000000000000000000000000000000000000000000) ;
   iv := [("x1",
-    ((-157)/(50),
-    (157)/(50)))];
+    ((1)/(100),
+    (3)/(4)))];
   |>
 End
 
diff --git a/testcases/timing/cert_xu2_cosScript.sml b/testcases/timing/cert_xu2_cosScript.sml
index 1d51914fab85e8d14aa15bd353471acc363ea136..6ae8e42c684d55303629ff0cfe6458ff13788aee 100644
--- a/testcases/timing/cert_xu2_cosScript.sml
+++ b/testcases/timing/cert_xu2_cosScript.sml
@@ -10,17 +10,17 @@ Definition cos_example_def:
   <|
     transc := Fun Cos (Var "x2");
     poly := [
-    (97091928396572901860395177209284156560897827148437)/(100000000000000000000000000000000000000000000000000);
-    (88102801838149783110816523083508094646432162733163)/(500000000000000000000000000000000000000000000000000000000000);
-    (-124817476790713)/(281474976710656);
-    (-47340982058707618492410287079998933157387597248089)/(1000000000000000000000000000000000000000000000000000000000000);
-    (125000945627423811282175059034216246800497174263)/(5000000000000000000000000000000000000000000000000);
-    (14944574916626695440490972902893799384438366928407)/(5000000000000000000000000000000000000000000000000000000000000)
+    (1)/(1);
+    (-4379281)/(4398046511104);
+    (-2097031)/(4194304);
+    (-4623463)/(17179869184);
+    (2869529)/(67108864);
+    (-4326429)/(2147483648)
     ];
-  eps := (60325149764354696387657436231227704193819721325461)/(2000000000000000000000000000000000000000000000000000) ;
+  eps := (66768433028906857241364386230056457575537231426463)/(5000000000000000000000000000000000000000000000000000000000) ;
   iv := [("x2",
-    ((-157)/(50),
-    (157)/(50)))];
+    ((1)/(100),
+    (1)/(2)))];
   |>
 End
 
diff --git a/testcases/timing/cert_xu2_sinScript.sml b/testcases/timing/cert_xu2_sinScript.sml
index ef46394a3dcc87fb0f2621ab358fc2a9738b3d70..e150c9ad49480316b55652bb4a6af773d921fa3a 100644
--- a/testcases/timing/cert_xu2_sinScript.sml
+++ b/testcases/timing/cert_xu2_sinScript.sml
@@ -10,17 +10,17 @@ Definition sin_example_def:
   <|
     transc := Fun Sin (Var "x2");
     poly := [
-    (-3458420040541902157599986648920916201821462721)/(6250000000000000000000000000000000000000000000000000000);
-    (9844584217973025852543855762633029371500015258789)/(10000000000000000000000000000000000000000000000000);
-    (11948551839482203120988263353690998769263131862317)/(10000000000000000000000000000000000000000000000000000000000);
-    (-153486018610747773638358637526835082098841667175293)/(1000000000000000000000000000000000000000000000000000);
-    (-5981023209126048755582390573250608015176688070369)/(25000000000000000000000000000000000000000000000000000000000);
-    (13669493890370461829097958883494356996379792690277)/(2500000000000000000000000000000000000000000000000000)
+    (1702239)/(281474976710656);
+    (2097151)/(2097152);
+    (5026859)/(549755813888);
+    (-87417)/(524288);
+    (7684211)/(34359738368);
+    (4318107)/(536870912)
     ];
-  eps := (1020940859788826944075336902524496760092532056821)/(125000000000000000000000000000000000000000000000000) ;
+  eps := (1022402505584581323545407424568064469905824764589)/(312500000000000000000000000000000000000000000000000000000) ;
   iv := [("x2",
-    ((-157)/(50),
-    (157)/(50)))];
+    ((1)/(100),
+    (1)/(2)))];
   |>
 End