Jongwook_Kim

Unsoundness bug with smt2 file over arctan2 function.

5

With the following input, and precision=0.001 : (set-logic QF_NRA) (declare-fun x () Real) (declare-fun y () Real) (declare-fun z () Real) (declare-fun s1 () Real [1.0,4.0]) (declare-fun s2 () Real...

Soundness Bug with QF_NRA formula.

1

(declare-fun c () Real) (declare-fun d () Real) (assert (

How to convert smt2 file to AST?

2

I would like to use function that convert smt2 file to AST(abstract syntax tree) in python API. Can I use these functions in dreal? If so, Can you please point...

[consolidate] (smt.string_solver=z3str3) Refutation Soundness issue on String Theory

2

Hi, For following formula, z3str3 9d9414c1110bc65108202cdcc473c703d12b54f1 returns unsat but z3 returns sat. I confirm this formula is satisfiable and z3 is correct. I seems this bug is caused by z3str3...

(smt.string_solver=z3str3) str.is_digit function issue

1

Hi, For this formula, z3str3 d61d0f6a66b3874e247d8f8396bd86ffc0dee05e gives an invalid model. It seems ``str.is_digit`` and ``str.from_code`` function is root cause. If an integer is entered as a parameter of ``str.from_code``, then...