Shaobo
Shaobo
> Another minor point: `RealToInt` is a strange name to me, why not calling it `Floor`? `Floor` indeed makes more sense as it reflects the semantics of this operation. However,...
> @shaobo-he Thanks for the contribution. > > Before accepting this PR, we need to add the new operator also to all other solvers supporting QF_LIRA (mathsat, CVC4 and yices),...
Hi, @mikand. I updated this PR. Please take a look at it again and let me know if it needs any changes.
Thank you for your feedback. > Also, note that the logic addition code is incomplete: you also need to extend the TheoryOracle in oracles.py to produce non-linearity when it encounters...
Hello, @mikand. I'm sorry to bother you again. I was wondering if there's any feedback or decision on this PR. I'd like to see this PR merged so that I...
> > The syntax of creating a floating-point constant node. > > How is this done in SMT-LIB? How is this done in z3? These are typically things we look...
Can we have c regressions first?
> Is this because LLVM maybe compiles away these assertions or something like that? What is the root cause of this? Is the generated Boogie file ok? No, this is...
Follow-up: this is because `RemovePtrToIntPass` eliminates the `ptrtoint` operation but not `inttoptr` as well. So we have only one complicated node.
One solution is to inline foo manually.