SAW C verification example fail

Question

In the document SAWScript Galois, is an example of verifying a dot product implementation. I get an error:

dotprod.c:

#include <stdint.h>
#include <stdlib.h>

uint32_t dotprod(uint32_t *x, uint32_t *y, uint32_t size)
{
    uint32_t res = 0;
    for(size_t i = 0; i < size; i++) {
        res += x[i] * y[i];
    }
    return res;
}

dotprod.saw:

import "dotprod.cry";
m <- llvm_load_module "dotprod.bc";


xs <- fresh_symbolic "xs" {| [12][32] |};
ys <- fresh_symbolic "ys" {| [12][32] |};
let allocs = [ ("x", 12), ("y", 12) ];
let inputs = [ ("*x", xs, 12) , ("*y", ys, 12) , ("size", {{ 12:[32] }}, 1)     ];
let outputs = [(" return", 1)];

t <- llvm_symexec m "dotprod" allocs inputs outputs true;
thm1 <- abstract_symbolic {{ t == dotprod xs ys }};
prove_print thm1;

The SAW script give the error:

Loading module Cryptol
Loading file "dotprod.saw"
Loading module Main
saw: user error (Bitcode parsing of inc_file.bc failed:
not implemented
  from:
    FUNC_CODE_INST_GEP
    dotprod
    FUNCTION_BLOCK
    MODULE_BLOCK)

I use:

• SAW version 0.2
• cryptol version 2.5.0
• clang version 3.7

Update 1:

SAW was recompiled from its git repository and I am using stack version 1.5.1.

After updating the error changed to:

Loading module Cryptol
Loading file "... /dotprod.saw"
Loading module Main
saw: user error ("llvm_symexec" (... /dotprod.saw:11:6):
"Parse error: \"expr\" (line 1, column 1):\nunexpected \" \"\nexpecting   \"*\", \"return\", \"args[\", letter, \"_\" or \"(\"")

Answer 1

The question was answered on the project's git site

The solution snippet

let outputs = [("return", 1)];

t <- llvm_symexec m "dotprod" allocs inputs outputs true;
thm1 <- abstract_symbolic {{ t == dotprod xs ys }};
prove_print abc thm1;