search

conjure-cp / conjure-notebook

3 stars 2 forks source link

Error when using yices-bv #18

Open sasha704 opened 1 year ago

sasha704 commented 1 year ago 
%%conjure
find x: int(0..5)

When using yices-bv, produces output:

Exception: Error:
    Savile Row stdout: Created output file for domain filtering conjure-output/model000001.eprime-minion
Created output SMT file conjure-output/model000001.eprime-smt

    Savile Row stderr: ERROR: boolector exited with error code:19 and error message:
yices-smt2: invalid option: -m
Try yices-smt2 --help for more information

    Savile Row exit-code: 1