--- a/trunk/Toss/Solver/Solver.ml
+++ b/trunk/Toss/Solver/Solver.ml
@@ -259,7 +259,7 @@
     | Char phi ->
       let fv = FormulaSubst.free_vars phi in
       if List.exists (function `FO _ -> false | _ -> true) fv then
-        failwith "non first-order free vars in real_expr not yet supported"
+        failwith "non first-order free vars/consts in real_expr not allowed yet"
       else List.rev_map to_fo fv
     | Sum (vl, _, r) ->
       List.filter (fun w -> not (List.mem w vl)) (fo_vars_r_rec r)
@@ -382,9 +382,13 @@
 (* Evaluate with assignment, no cache. *)
 let evaluate_partial_aset solver ~formula struc fo_aset =
   let elems = Assignments.set_to_set_list (Structure.elems struc) in
+  let cvs, cels = List.split (Structure.constants struc) in
+  let consts_asg = if cvs = [] then Any else
+      assignments_of_list elems (Array.of_list cvs) [Array.of_list cels] in
+  let asg = join fo_aset consts_asg in
   let phi = Hashtbl.find solver.formulas_eval formula in
   incr eval_counter;
-  eval [] struc elems fo_aset phi
+  eval [] struc elems asg phi
 
 (* Helper: find assoc and remove. *)
 let rec assoc_del (x : Formula.formula) = function
@@ -576,10 +580,6 @@
       res
     with Not_found ->
       LOG 1 "Eval_m %s" (str phi);
-      (*let atoms = FormulaMap.get_atoms phi in
-      let full_so_atom = function (* FIXME!!! should be non-fp vars *)
-        | Formula.SO (_, a) -> Array.length a > 1 | _ -> false in
-      if List.exists (fun a -> full_so_atom a) atoms then *)
       let fv = FormulaSubst.free_vars phi in
       let fq_vars = List.rev_append fv (FormulaSubst.quantified_vars phi) in
       if List.exists (fun v -> Formula.is_so v) fq_vars then (
@@ -593,7 +593,10 @@
       ) else (
         let els = Assignments.set_to_set_list (Structure.elems struc) in
         check_timeout "Solver.eval_m.not_found_noso";
-        let asg = eval [] struc els Any phi in
+        let cvs, cels = List.split (Structure.constants struc) in
+	let consts_asg = if cvs = [] then Any else
+            assignments_of_list els (Array.of_list cvs) [Array.of_list cels] in
+        let asg = eval [] struc els consts_asg phi in
         incr eval_counter;
         Hashtbl.add !cache_results phi (asg, phi_rels phi);
         asg
@@ -703,19 +706,24 @@
 			 Assignments.str ev_assgn) in
       get_rval (join asg (evaluate_real "#" expr struc))
 
-let rec get_real_val_cache ?(asg=Any) solver struc = function
+let rec get_real_val_cache asg solver struc = function
   | Const c -> c 
   | Plus (e1, e2) ->
-    (get_real_val_cache ~asg solver struc e1) +.
-      (get_real_val_cache ~asg solver struc e2)
+    (get_real_val_cache asg solver struc e1) +.
+      (get_real_val_cache asg solver struc e2)
   | Times (e1, e2) -> 
-    (get_real_val_cache ~asg solver struc e1) *.
-      (get_real_val_cache ~asg solver struc e2)
+    (get_real_val_cache asg solver struc e1) *.
+      (get_real_val_cache asg solver struc e2)
   | Pow (e1, e2) ->
-    (get_real_val_cache ~asg solver struc e1) **
-      (get_real_val_cache ~asg solver struc e2)
+    (get_real_val_cache asg solver struc e1) **
+      (get_real_val_cache asg solver struc e2)
   | re ->
     update_cache struc;
+    let cvs, cels = List.split (Structure.constants struc) in
+    let els = Assignments.set_to_set_list (Structure.elems struc) in
+    let consts_asg = if cvs = [] then Any else
+        assignments_of_list els (Array.of_list cvs) [Array.of_list cels] in
+    let asg = join asg consts_asg in
     try
       let (res, _) = Hashtbl.find !re_cache_results (re, asg) in
       LOG 2 "found in re cache: %s" (Formula.real_str re);
@@ -759,7 +767,10 @@
   let check struc phi = check_cache (
     check solver ~formula:(register_formula_s struc solver phi) struc)
   let get_real_val ?asg re struc = 
-    check_cache (get_real_val_cache ?asg solver struc re)
+    let asg = match asg with 
+      | None -> Any
+      | Some a -> a in
+    check_cache (get_real_val_cache asg solver struc re)
 
   let set_timeout t = timeout := t
   let clear_timeout () = timeout := (fun () -> false);