search

yav / simple-smt

BSD 3-Clause "New" or "Revised" License
20 stars 20 forks source link

yices-smt2 sometimes returns real value without decimal point #20

Open jwaldmann opened 2 years ago

jwaldmann commented 2 years ago

well, it's an edge case, but here goes:

[send->] (get-value (v15))
[<-recv] ((v15 0.0))    -- fine, has decimal point

[send->] (get-value (0.0))
[<-recv] ((0.0 0))       -- not fine

this sometimes happens in my application (some expressions might have been simplified but I do not keep track of it)

cvc5 sends back 0.0.

It's a bit hard to fix in simple-smt, since getExprs is not typed. I can fix it in my application https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/commit/a9dd4017030d7992132de745708ebfb2cabd51fb because I have typed expressions there.

yav commented 2 years ago

Agreed that this sort of thing should probably be handled in the application using simple-stm. Do we need to do something for this ticket?