latest version of dReal3 (2015 May) returns different result for the first example

[soonhokong]

@zenna, FYI, I'm investigating this issue. It works fine with the released version (2015 Mar).

using dReal
x = Var(Int,"x")
y = Var(Int,"y")
add!((x > 2) & (y < 10) & (x + 2*y == 7))
is_satisfiable()

[soonhokong]

2015 May version gives unsat for this example. I've added a C version of the same example: https://github.com/dreal/dreal3/blob/master/src/tests/c_api/dreal_jl_01.c. It gives the right result (sat).

[zenna]

@soonhokong To fix this I tried to build the latest dReal (using build_dreal_only.sh) but get errors on compilation when it gets to building JSON stuff:

src/json.hpp:1286:44: error: no matching function for call to ‘std::vector<nlohmann::basic_json<> >::erase(__gnu_cxx::__normal_iterator<const nlohmann::basic_json<>*, std::vector<nlohmann::basic_json<> > >&)’

Whole error log is here https://gist.github.com/zenna/af996a4aeb997805d695

[soonhokong]

I had the same issue and reported it to nlohmann/json#68. I updated https://github.com/dreal-deps/json to avoid the problem. Please do the following in the build directory:

rm -rf external/src/JSON*
rm -rf external/tmp/JSON*
make

If you still have a problem, please let me know.

[zenna]

Still getting the JSON error. Did you push your changes?

On 4 May 2015 at 19:19, Soonho Kong notifications@github.com wrote:

I had the same issue and reported it to nlohmann/json#68
nlohmann/json#68. I updated
https://github.com/dreal-deps/json to avoid the problem. Please do the
following in the build directory:

rm -rf external/src/JSON*
rm -rf external/tmp/JSON*
make

If you still have a problem, please let me know.

—
Reply to this email directly or view it on GitHub
#2 (comment).

[soonhokong]

I did something but it seems that it's not enough. Could you try to install g++-4.9 and use it? I found that that can be a workaround. If you're using Ubuntu, it is available via apt-get.

[soonhokong]

I found some problems when we handle unbounded problems. I think solving that problem will resolve this issue.

[soonhokong]

@zenna, could you take a look at my patch https://github.com/soonhokong/dReal.jl/commit/e2a180d5a93d441fcf959b55f7857f3c991ece18?

We have a mismatch between the C function declaration for opensmt_mk_int_var and Julia's interface. Recently, I've changed opensmt_mk_int_var to take long arguments while Julia's interface is still expecting Cint. As a result, when we pass [intmin, intmax] to C API, the values got type casted and end up with empty interval.

[zenna]

Looks good. Yes I should have fixed this earlier. Did this fix the issue?

[soonhokong]

For this particular example, yes, it fixed the problem. I haven't tested other examples, yet.

[soonhokong]

Dear @zenna,

• I just updated the release page with a new shared library (v3.15.05 / for 64-bit Linux).
• Do you think it's fine to merge https://github.com/soonhokong/dReal.jl/commit/e2a180d5a93d441fcf959b55f7857f3c991ece18? If it's OK, let's merge it to this repository.

[soonhokong]

For the first item, I just updated README.md by a28615c.

[zenna]

Yes. Merge them. Feel free to commit to directly to master.

On 6 May 2015 at 09:54, Soonho Kong notifications@github.com wrote:

For the first item, I just updated README.md by a28615c
a28615c
.

—
Reply to this email directly or view it on GitHub
#2 (comment).

[soonhokong]

Fixed by 1d340f6.