JavaScript examples

[NikolajBjorner]

There is something fishy with JS example with multiple results. The pre-compiled output looks fine, but running them after adding dummy space results in errors. Example,

Error: z3-js-web failed with input:
// bitvectors: simple proofs
const x = Z3.BitVec.const('x', 32);

const sConj = x.sub(10).sle(0).eq(x.sle(10));
const sSolver = new Z3.Solver();
sSolver.add(sConj);
await sSolver.check(); // sat

const sModel = sSolver.model();
sModel.get(x) // signed

const uConj = x.sub(10).ule(0).eq(x.ule(10));
const uSolver = new Z3.Solver();
uSolver.add(uConj);
await uSolver.check(); // sat

const uModel = uSolver.model();
uModel.get(x) // unsigned

error:
TypeError: i.output.match is not a function

[rlisahuang]

The issue was that the result of this snippet is an object, whereas we want its String representation. It revealed a bug that we never did stringified outputs when running Z3 from the web (smtlib or JS). Fixed in the the most recent commit on main.