[PA] Derive Z3 sort for labeled result/stub pair

...from the sort of the concrete disjuncts, which is sound on any proper, terminating programs. Test plan: `dune test program_analysis` ghstack-source-id: 1cb642277581ab149315dc7550470c936a0c8a0a Pull Request resolved: #91
JHU-PL-Lab · Jul 18, 2023 · 6220027 · 6220027
1 parent 3b99a69
commit 6220027
Show file tree

Hide file tree

Showing 10 changed files with 131 additions and 579 deletions.
diff --git a/interpreter/src/ast.ml b/interpreter/src/ast.ml
@@ -117,7 +117,7 @@ let next_label = ref 0
 
 let get_next_label () =
   let l = !next_label in
-  next_label := l + 1;
+  incr next_label;
   l
 
 let reset_label () = next_label := 0