More info about bundled z3.js

[esad]

Hi,

I'm trying to compile z3 with emscripten to use it in another project.

I started with your version of z3.emscripten.js - and it worked fine. However, when I later tried to build my own version of z3 (that supports soft constraints) - it built fine but segfaults on certain queries :( Your original version (based on 4.3.1 as far as I can tell) works fine though, although it doesn't support assert-soft that was introduced in v4.4.1.

Do you mind providing more information on which upstream commit the bundled z3.js is based and which emscripten configuration was used to build it so I can have a starting point of a working build and see where things went wrong?

[timfel]

I have extracted the steps to compile the version that is currently bundled with babelsberg.js into a shell script: https://github.com/babelsberg/z3.js/blob/master/build_z3.sh

I, too, have had problems with newer versions not working properly, although I did have a version with soft constraints working at one point (don't know where I put it though). The main problem was that the version with soft constraints crashed or returned unsat significantly more often for me than the version that is bundled with babelsberg.js.

[esad]

Hi Tim,

first of all thanks for all the work you did so far on bringing z3 to the browser, it was a great starting point!

The problem with build_z3.sh from the z3.js repo is that it uses the "latest" emscripten and z3, and I think it's the particular mix of emscripten optimizations and the z3 codebase that makes code crash (or work) - that's why I was interested in which exact version was used to build the emscripten version in this repository.

[timfel]

Uh, I don't remember, unfortunately - at the time it was an experiment and it just worked right of the bat with whichever version was latest at the time, and I never bothered to document it, because at the time I assumed if the first thing I tried worked, than any other version would work, too