annotate final_pre/src/cbmc-assert.c @ 10:a01801c32db7

fix final_pre
author ryokka
date Tue, 20 Feb 2018 17:35:52 +0900
parents 28f900230c26
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
7
28f900230c26 add final_pre
ryokka
parents:
diff changeset
1 void verifySpecification(struct Context* context,
28f900230c26 add final_pre
ryokka
parents:
diff changeset
2 struct Tree* tree) {
28f900230c26 add final_pre
ryokka
parents:
diff changeset
3 assert(!(maxHeight(tree->root, 1) >
28f900230c26 add final_pre
ryokka
parents:
diff changeset
4 2*minHeight(tree->root, 1)));
28f900230c26 add final_pre
ryokka
parents:
diff changeset
5 return meta(context, EnumerateInputs);
28f900230c26 add final_pre
ryokka
parents:
diff changeset
6 }
28f900230c26 add final_pre
ryokka
parents:
diff changeset
7