Merge pull request #1629 from GaloisInc/heapster/prover-tests-ci

Add prover tests to CI
GaloisInc · Apr 20, 2022 · 28d8675 · 28d8675
2 parents 09889af + 342bb74
commit 28d8675
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -135,6 +135,7 @@ jobs:
           targets: |
             integration_tests
             cryptol-saw-core-tc-test
+            prover_tests
           dest: dist-tests
 
       - uses: actions/upload-artifact@v2

diff --git a/heapster-saw/proverTests/Main.hs b/heapster-saw/proverTests/Main.hs
@@ -133,10 +133,10 @@ int32array :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (
 int32array off len = Perm_LLVMArray (int32ArrayPerm off len)
 
 int64ArrayPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> LLVMArrayPerm 64
-int64ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 8 (fieldShape (intValuePerm @ 64))
+int64ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 8 (fieldShape (intValuePerm @64))
 
 int32ArrayPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> LLVMArrayPerm 64
-int32ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 4 (fieldShape (intValuePerm @ 32))
+int32ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 4 (fieldShape (intValuePerm @32))
 
 arrayPerm ::
   PermExpr (BVType w) ->