xxxx@xxx:~/Develop/smt$ cat arm-crkme-1.b read10str.c

(declare-const a0 (_ BitVec 32))
(declare-const a1 (_ BitVec 32))
(declare-const a2 (_ BitVec 32))
(declare-const a3 (_ BitVec 32))
(declare-const a4 (_ BitVec 32))

(assert (= #x69790439 (bvxor a0 #x12345678)))
(assert (= #xc2819e87 (bvadd a0 a1)))
(assert (= #xe91e0419 (bvsub a2 a1)))
(assert (= #xdd1f1d1c (bvsub a2 a3)))
(assert (= #xd07a8174 (bvadd a4 a3)))
(check-sat)

/* quick progam to convert 1s and 0s
 * output from boolector to string
 */

#include <stdio.h>
#include <stdlib.h>

int main(void)
{
	char *endptr, *line = NULL;
	size_t len = 0;
	ssize_t read;
	long val;
	long *intptr;

	// only read from stdin
	while ((read = getline (&line, &len, stdin)) != -1) {

		// lop off newline
		line[len-1] = 0;
		// convert binary to long
		val = strtol(line, &endptr, 2);
		intptr = &val;
		printf("%s", intptr);
	}
	printf("\n");
}
xxxx@xxx:~/Develop/smt$ boolector -m arm-crkme-1.b  | awk '{print $2}' | ./read10str
ARM{FL4G_PR0C33S1NG}