Circular decimal last char ‘?’ cannot parse decimal or double

[JavaScript-zt]

fix it plz

[HowardvanRooijen]

Can you provide some more details please?

[JavaScript-zt]

code ：

    using var ctx = new Z3Context();
    var theorem = from t in ctx.NewTheorem<(decimal sz, decimal bz)>()
                  where 0.1752m * t.sz + 0.1252m * t.bz >= 2500 
                  where 0.1221m * t.sz + 0.1084m * t.bz >= 1900 
                  where 0.2008m * t.sz + 0.1718m * t.bz >= 3000 
                  where 0.2209m * t.sz + 0.2428m * t.bz >= 3500 
                  where 0.2811m * t.sz + 0.3519m * t.bz >= 5000  
                  where 0 <= t.sz && t.sz <= 90000            
                  where 0 <= t.bz && t.bz <= 60000               
                  orderby (20.0m * t.sz) + (15.0m * t.bz)
                  select t;
    var (sz, bz) = theorem.Solve();

error line：

[HowardvanRooijen]

System.FormatException
  HResult=0x80131537
  Message=Input string was not in a correct format.
  Source=System.Private.CoreLib
  StackTrace:
   at System.Number.ThrowOverflowOrFormatException(ParsingStatus status, TypeCode type)
   at System.Decimal.Parse(String s, IFormatProvider provider)
   at Z3.Linq.Theorem.ConvertZ3Expression(Object destinationObject, Context context, Model model, Environment subEnv, MemberInfo parameter) in \Z3.Linq\solutions\Z3.Linq\Theorem.cs:line 439

[HowardvanRooijen]

We believe Z3 suffixes the decimal string with a ? to demonstrate it's been truncated.

https://github.com/Z3Prover/z3/blob/123c44639564455ff09490446b8c0abbca807533/src/util/mpq.cpp#L178-L181

If we trim off the ? then the theorum evaluates to:

sz: 8939.850354678845593236808862, bz: 7457.9729861043630356622291323

[HowardvanRooijen]

Fixed by 34435733c1fcb112f5903008eaac1ca11c549397 I have yet to set up a CLA - but once I do, would you be willing to submit your sample (with some comments about the problem it represents) to the repo?