let string_symbol_list = [("not", Symbol.mk_symbol `NOT); ("=>", Symbol.mk_symbol `IMPLIES); ("and", Symbol.mk_symbol `AND); ("or", Symbol.mk_symbol `OR); (* ("xor", Symbol.mk_symbol `XOR); *) ("=", Symbol.mk_symbol `EQ); (* ("distinct", Symbol.mk_symbol `DISTINCT); *) ("ite", Symbol.mk_symbol `ITE); ("-", Symbol.mk_symbol `MINUS); ("+", Symbol.mk_symbol `PLUS); ("*", Symbol.mk_symbol `TIMES); ("/", Symbol.mk_symbol `DIV); ("div", Symbol.mk_symbol `INTDIV); ("mod", Symbol.mk_symbol `MOD); (* ("abs", Symbol.mk_symbol `ABS); *) ("<=", Symbol.mk_symbol `LEQ); ("<", Symbol.mk_symbol `LT); (">=", Symbol.mk_symbol `GEQ); (">", Symbol.mk_symbol `GT); ("to_real", Symbol.mk_symbol `TO_REAL); ("to_int", Symbol.mk_symbol `TO_INT); (* ("is_int", Symbol.mk_symbol `IS_INT); *) (* ("bv-concat", Symbol.mk_symbol `CONCAT); ("bv-not", Symbol.mk_symbol `BVNOT); ("bv-neg", Symbol.mk_symbol `BVNEG); ("bv-and", Symbol.mk_symbol `BVAND); ("bv-or", Symbol.mk_symbol `BVOR); ("bv-add", Symbol.mk_symbol `BVADD); ("bv-mul", Symbol.mk_symbol `BVMUL); ("bv-div", Symbol.mk_symbol `BVDIV); (* ("bvurem", Symbol.mk_symbol `BVUREM); *) ("bv-shift-left0", Symbol.mk_symbol `BVSHL); ("bv-shift-right0", Symbol.mk_symbol `BVLSHR); ("bv-lt", Symbol.mk_symbol `BVULT); *) (* ("select", Symbol.mk_symbol `SELECT); *) ("update", Symbol.mk_symbol `STORE) ]