Merge pull request #40 from SoftwareFoundationGroupAtKyotoU/fix_SMT_o…

…utput

Follow the format change of SMT solvers.

.travis-ci.sh

@@ -2,14 +2,16 @@
 
 set -ev
 
-opam init --yes --no-setup --comp 4.08.0
-eval $(opam config env)
-opam install --yes menhir ppx_sexp_conv sexplib dune ppx_let ppx_custom_printf yaml
+# opam init --yes --no-setup --comp 4.08.0
+# eval $(opam config env)
+# opam install --yes menhir ppx_sexp_conv sexplib dune ppx_let ppx_custom_printf yaml z3
 
-mkdir -p ~/.local/bin
-export PATH=$HOME/.local/bin:$PATH
-curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-ubuntu-14.04.zip > z3.zip
-unzip -o -j z3.zip z3-4.8.4.d6df51951f4c-x64-ubuntu-14.04/bin/z3 -d ~/.local/bin
+# mkdir -p ~/.local/bin
+# export PATH=$HOME/.local/bin:$PATH
+# curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.12/z3-solver-4.8.12.0.tar.gz > z3.tar.gz
+# unzip -o -j z3.zip z3-4.8.12-x64-glibc-2.31/bin/z3 -d ~/.local/bin
+
+z3 -version
 
 # approximately the memory available on travis
 make -C ./src test.exe genFlags.exe stdlib/lin.intr

.travis.yml

@@ -1,3 +1,4 @@
+dist: bionic
 language: c
 addons:
   apt:
@@ -15,4 +16,13 @@ cache:
   directories:
     - $HOME/.opam
     - $HOME/jdk8
+
+before_install:
+- opam init --yes --no-setup --comp 4.08.0
+- eval $(opam env)
+
+install:
+- opam install --yes menhir ppx_sexp_conv sexplib dune ppx_let ppx_custom_printf yaml
+- travis_wait 30 opam install --yes z3
+
 script: bash -ex .travis-ci.sh

src/ownershipSolver.ml

@@ -170,7 +170,7 @@ let solve_ownership ~opts result =
       let open Sexplib.Sexp in
       let s = scan_sexp @@ Lexing.from_string m in
       match s with
-      | List (Atom "model"::model) ->
+      | List (Atom "model" :: model) | List model ->
         let model_assoc = extract_assoc model [] in
         let o_sigma = List.fold_left (fun acc (nm,ty,body) ->
             match ty,body with