Nikhil Loney

Hi, I am currently formalizing a simple system with ODEs in SMT2 and using dReal to solve it. I wanted to apply the invariant `not (x1)` to a particular mode...

Hi, I have recently moved to dReal from z3 due to its obvious advantage dealing with non-linear theories. However, for some of the problems I have been working on, I...