JBMC: adjust float expressions per function

smowton · Jan 24, 2018 · c91ff69 · c91ff69
1 parent eed983a
commit c91ff69
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
@@ -693,6 +693,9 @@ void jbmc_parse_optionst::process_goto_function(
 
     // add generic checks
     goto_check(ns, options, ID_java, function.get_goto_function());
+
+    // checks don't know about adjusted float expressions
+    adjust_float_expressions(goto_function, ns);
   }
 
   catch(const char *e)
@@ -730,9 +733,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // checks don't know about adjusted float expressions
-    adjust_float_expressions(goto_model);
-
     // ignore default/user-specified initialization
     // of variables with static lifetime
     if(cmdline.isset("nondet-static"))