Skip to content

Commit c3297ce

Browse files
committed
Use Z3_mk_fpa_sort_single instead of hardcoded values
1 parent 84f8bcd commit c3297ce

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/Interpreter/concolic_interpreter.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -787,7 +787,9 @@ bool ConcolicInterpreter::i_instr_conversion(Module *m, uint8_t opcode) {
787787
break; // i64.trunc_u/f64
788788
case 0xb2:
789789
// TODO: fpa_sort values
790-
m->symbolic_stack[m->sp] = sbv_to_fpa(m->symbolic_stack[m->sp].value(), m->ctx.fpa_sort(8, 24));
790+
//m->symbolic_stack[m->sp].value().mk_from_ieee_bv(m->ctx.fpa_sort(8, 24));
791+
m->symbolic_stack[m->sp] = sbv_to_fpa(m->symbolic_stack[m->sp].value(), z3::to_sort(m->ctx, Z3_mk_fpa_sort_single(m->ctx)));
792+
//m->symbolic_stack[m->sp] = sbv_to_fpa(m->symbolic_stack[m->sp].value(), m->ctx.fpa_sort(8, 24));
791793
break; // f32.convert_s/i32
792794
case 0xb3:
793795
// TODO: Symbolic semantics

0 commit comments

Comments
 (0)