linux-vdso.so.1 =>  (0x00007ffda9aa0000)
	libz3.so => /usr/lib/libz3.so (0x00007f7599d26000)
	libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f75999d0000)
	libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f75997cc000)
	libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f75993ec000)
	librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007f75991e4000)
	libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f7598e5e000)
	libgomp.so.1 => /usr/lib/x86_64-linux-gnu/libgomp.so.1 (0x00007f7598c2f000)
	libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f7598a18000)
	libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f75987f9000)
	/lib64/ld-linux-x86-64.so.2 (0x00007f759b757000)
undefined symbol: Z3_solver_from_file	(./rshfor.native)
undefined symbol: Z3_mk_select_n	(./rshfor.native)
undefined symbol: Z3_get_parser_error	(./rshfor.native)
undefined symbol: Z3_mk_as_array	(./rshfor.native)
undefined symbol: Z3_mk_bv_numeral	(./rshfor.native)
undefined symbol: Z3_solver_from_string	(./rshfor.native)
undefined symbol: Z3_mk_array_sort_n	(./rshfor.native)
undefined symbol: Z3_mk_store_n	(./rshfor.native)