次回に向けて、はやくも落ち穂拾い。 double intだけでなくdoubleでも使えるか、確認。 #include <stdio.h> #include <stdlib.h> #include <assert.h> int main (int argc, char **argv) { int _rand = rand(); double r; #ifdef __CBMC__ __CPROVER_assume(0 <= _rand && _rand <= RAND_M</assert.h></stdlib.h></stdio.h>…