Florian Schanda

Also, for some of these the platform of the computer I am on seems to matter. wintersteiger/mul/mul-has-no-other-solution-15884.smt2 for example returns SAT on my AMD computer but UNKNOWN on my Intel...

Some of the issues could be resolved by not using -march=native that the CMakeLists hard-codes. However the bulk of the issued described above remain.

Thank you for the fast fixes :) I am currently re-running our benchmark suite and will let you know if anything new pops up. I think it would be good...

Results are different now, we've found 4970 unsound answers, but they are not the same ones as before. Below a *reduced* list, but it should cover everything. ``` crafted/QF_FP/why3_review_01.smt2 nyxbrain/crafted-edge-cases/RNE:gt_to_lt_unsat.smt2...

The Z3 parser is correct, the comparison is SMTLIB =, not FP EQ. I believe your workaround is only going to add unsoundness when benchmarks depend on subtle difference between...

I should further note that the SMTLIB floating point standard makes this distinction, and several benchmarks depend on this.

@mriesch-tum and @davidvarga I have managed to write a fully working MATLAB lexer and parser (https://github.com/florianschanda/miss_hit), and I plan to write down the formal grammar sometime soon.

At the risk of spamming in every ticket here; writing a fully working MATLAB lexer is an insane activity. Please refer to this for my analysis on this, if you...

@niklasnylen do you have any thoughts on this? The idea is you can do extra things for e.g. just changed files on checkin.

@niklasnylen that might also be a good idea, but I think it should be phrased as templates or defaults. Configuration works by having a magic object containing all the options....