Wrong results for simple formulas

[dtraytel]

Wrong results for simple formulas

[tfiedor]

Dear Dmitriy,

thank you for your interest in our approach. The tool is still prototype and during october we implemented the new version, which needs lots of optimizations and is not fully tested, so there may be some bugs. I don't see problem in the syntax, but during the evaluation we didn't work with formulae without variables and with free variables.

I will look more deeply into this formulae in few weeks, as I am currently occupied with different research.

Best regards,
Tomas Fiedor.

[dtraytel]

Dear Tomas,

thanks for the quick reply!

Just for the record, ground formulas with superfluous quantifier, e.g.

all1 a0, a1: a0 = a0;

also currently give unexpected results.

If you wonder why and how I get those funny formulas: I was performing random testing on my own inefficient and tiny implementation (https://github.com/dtraytel/WS1S), and simultaneously trying different tools as well.

Best wishes,
Dmitriy