Lev Nachmanson
Lev Nachmanson
Submitted by mistake.
Here some first observations. In the current master the long run does not happen but instead I get an "unknown". It seems it is extremely rare occurrence as well. Running...
Here is the fixed test with some comments. A couple of points to make here are that Graph contains Graphs and Nodes, and Edge is just a pair of Nodes....
I think I fixed it with the last commit. I also published the new npm packages.
Please create a pull request with a change that you prefer.
Fixed by [887ecc0](https://github.com/Z3Prover/z3/commit/887ecc0c98345533ab1ba28003d4e79fefd351c5). There was a previous fix in nlsat that moved the perf bottleneck from nlsat to grobner. I introduced a parameter that allows throttle grobner method aggressively, that...
@mtzguido, thank you for analysis! It seems the algorithm calculating a resultant was creating huge numbers. It might be worth looking if there is a more efficient algorithm in Cohen's...
try adding (get-model) as the very last command in your smt file.
It seems that z3 does not terminate in reasonable time on this benchmark. Reopening the issue.