diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index e2fb7fe5a..102a96ac5 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -146,7 +146,7 @@ namespace Microsoft.Z3
         /// The query is satisfiable if there is an instance of some relation that is non-empty.
         /// The query is unsatisfiable if there are no derivations satisfying any of the relations.
         /// </summary>        
-        public Status Query(FuncDecl[] relations)
+        public Status Query(params FuncDecl[] relations)
         {
             Contract.Requires(relations != null);
             Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
@@ -262,7 +262,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Convert benchmark given as set of axioms, rules and queries to a string.
         /// </summary>                
-        public string ToString(BoolExpr[] queries)
+        public string ToString(params BoolExpr[] queries)
         {
 
             return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9c054830c..ef1cd5f0a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1163,10 +1163,12 @@ public:
     }
         
     rational get_value(theory_var v) const {
-
+        
         if (v == null_theory_var || 
-            v >= static_cast<theory_var>(m_theory_var2var_index.size())) 
+            v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
+            TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
             return rational::zero();
+        }
             
         lp::var_index vi = m_theory_var2var_index[v];
         if (m_variable_values.count(vi) > 0)
@@ -1207,6 +1209,7 @@ public:
         if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
             reset_variable_values();
             m_solver->get_model(m_variable_values);
+            TRACE("arith", display(tout););
         }
     }
 
@@ -2642,6 +2645,7 @@ public:
         }
         else {
             rational r = get_value(v);
+            TRACE("arith", tout << "v" << v << " := " << r << "\n";);
             if (a.is_int(o) && !r.is_int()) r = floor(r);
             return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
         }