Proof search bugfix

eashanhatti · Jul 2, 2022 · 4539158 · 4539158
1 parent a7498dd
commit 4539158
Show file tree

Hide file tree

Showing 16 changed files with 7,826 additions and 479 deletions.
diff --git a/OUTPUT.c b/OUTPUT.c
@@ -1,2 +1,2 @@
-int f(int x) { return x; }
+int f(int x) { return (1 + x); }
 int g(int x) { return x; }
diff --git a/examples/c_compiler.per b/examples/c_compiler.per
@@ -22,7 +22,7 @@ axiom compile_add:
   ,  CompileTerm(`e2, `t2)
 axiom compile_zero: CompileTerm(zero, "0")
 axiom compile_one: CompileTerm(one, "1")
-axiom compile_var: Forall(t: Text), CompileTerm(var(t), t)
+axiom compile_var: CompileTerm(var(`t), `t)
 
 axiom CompileDecl: MetaFun(CDecl, Text) -> MetaType
 axiom compile_func: