Nikolaj Bjorner

Thanks, the workaround would be to pull from the tag. It has to be related to how the Nightly script (https://github.com/Z3Prover/z3/blob/master/scripts/nightly.yaml) is set up and interoperates with storing the state...

I looked into this a little, but simple changes to the build script didn't help. The sources are uploaded as a side-effect by a module with several parameters whose entry-level...

Logged question: https://developercommunity.visualstudio.com/content/problem/635723/updating-both-github-sources-and-assets-using-gith.html

@veanes - this relates to regex performance. FYI @cdstanford

BTW, I noticed that default build under nmake defines Z3DEBUG but not _TRACE. The previous behavior is to enable TRACE in debug builds.

Another note: I am currently unable to complete the nmake build on windows: ['C:/cmake/z3/src/api', 'api_ast_map.h'] Traceback (most recent call last): File "C:/cmake/z3/scripts/mk_gparams_register_modules_cpp.py", line 38, in sys.exit(main(sys.argv[1:])) File "C:/cmake/z3/scripts/mk_gparams_register_modules_cpp.py", line 32,...

I have a local fix which is to add a disjunction to the assert. The rest of the code seems ok

Some notes for diagnosis: - it diverges/converges with smt.arith.solver=6 depending on the value of smt.random_seed. So for many values of smt.random_seed it diverges by creating a cascade of (useless) cuts....

It appears to be a bit too early to test the change, but once we have figured this out it will be good with a more comprehensive validation, especially on...

https://github.com/Z3Prover/z3/releases/tag/Nightly