Stéphane Graham-Lengrand
Stéphane Graham-Lengrand
When interacting with Yices purely through the API, I think the only way to know which assertions have been added to a Yices context (which in that respect is somewhat...
libffi is installed on my Ubuntu 18.04 ``` /usr/share/info/libffi.info.gz /usr/share/doc/libffi6 /usr/share/doc/libffi-dev /usr/share/doc-base/libffi /usr/lib/x86_64-linux-gnu/libffi.a /usr/lib/x86_64-linux-gnu/libffi.so.6.0.4 /usr/lib/x86_64-linux-gnu/libffi.so /usr/lib/x86_64-linux-gnu/pkgconfig/libffi.pc /usr/lib/x86_64-linux-gnu/libffi_pic.a /usr/lib/x86_64-linux-gnu/libffi.so.6 ``` Compiling with regular 4.11.2+flambda finds it without problem. Compiling with 4.11.2+musl+static+flambda...
The assertion failure can be reached via the API. Pseudo SMT2 syntax to reproduce the sequence of API calls: ``` (set-logic mcsat) (declare-sort p 0) (declare-fun f (p) (Array p...
Minimal counter-example: ``` (set-logic all) (declare-sort p 0) (declare-fun s () p) (declare-fun p (p) p) (assert (and (= (p s) (_ Const 1 p)) (= (_ Const 2 p)...
So far, external SAT-solvers are only available through yices_check_formula / yices_check_formulas which don't use any Yices context; the assertions are just passed as arguments. At the moment if I have...
There's a corner case I've just discovered: If the type is the unit type (scalar type of cardinality 1), yices_new_uninterpreted_term returns the unique inhabitant of the type. It's satisfiability-preserving, but...
Minor point: Currently, Modules.scan_tree inspects all of the current directory and subdirectories, including my .git and my huge benchmark directory. Both are normally ignored by ocamlbuild because I put -traverse,...
Just to record it on github: ``` a: theory begin t : type t2 : type interface : [ t -> setof[t2]] end a b: theory begin t2 : type...