objective oriented optimization fails

[AnakinCN]

I've wrote this optimizaiton process to solve a ZenDecision object for me:

public static void Solve()
    {
        var naiveDecision = Zen.Symbolic<ZenDecision>();
        var solverConfig = new ZenLib.Solver.SolverConfig
        {
            SolverType = SolverType.Z3,
            SolverTimeout = TimeSpan.FromSeconds(10),
        };

               
        var solution = Zen.Maximize(
            Distance(naiveDecision),
            subjectTo: True(),
            config: solverConfig
        );
        bool satisfiable = solution.IsSatisfiable();   //true
        var result = solution.Get(naiveDecision);    
        Debug.WriteLine(result.Distance);      // always outputs 0 here, which is not expected
    }

    private static Zen<Real> Distance(Zen<ZenDecision> zenDecision)
    {
        Zen<Real> distance = zenDecision.GetField<ZenDecision, Real>("Distance");
        return distance;
    }

where ZenDecision is:

[ZenObject]
public class ZenDecision
{
    public FSeq<Real> GridRows { get; set; }
    public FSeq<Real> GridCols { get; set; }
    public ZenDecision()
    {
        //add 3 random elements into GridRows , they are ordered
        GridRows = addElements(3);
        //add 7 random elements into GridCols , they are ordered
        GridCols = addElements(7);
        //Distance = (Real)(Random.Shared.NextSingle() * 10000f);
        Distance = (Real)255;  //determined objective value
    }
    private FSeq<Real> addElements(int num)
    {
        FSeq<Real> elements = new(num);
        float[] array = new float[num];
        for (int i = 0; i < num; i++)
        {
            array[i] = Random.Shared.NextSingle();
        }
        //make elements ordered
        System.Array.Sort(array);
        for(int i = 0; i < num; i++)
        {
            elements.AddFront((Real)array[i]);
        }
        return elements;
    }
    public Real Distance
    {
        get ;
        set ;
    }
}

According to my understanding, the result.Distance should be big, either generated by ctor ZenDecision() or Zen searching, don't know why it is always 0. Did I miss something?