dreal3
dreal3 copied to clipboard
dreal
There is a new version of dReal, available at https://github.com/dreal/dreal4
I followed the instructions, but the compilation process failed on a newly created Ubuntu 14.04. The issue seems to occur when compiling MTIDD. I also tried to compile dreal on...
It happens since MTIDD was added. I have only seen this issue under linux machines with older versions of GCC (4.9 and 5.3). Instead of linking statically, dReal links against...
Dear dReal developers, is there an SMT2 parser in the dReal project which can be used together with the C-API? I mean somehing similar to the `parse_smt2_string()` function provided by...
There is a memory leak in translate_enode_to_exprnode. I believe it exhibits itself in many different ways, but to be concrete, imagine the expression (+ 1 2) is being processed. This...
Arif reported it. https://github.com/dreal/dreal3/blob/master/src/tests/drh/arif.drh ```bash dReach -k 1 arif.drh ``` It gives us an immediate unsat result because the generated `.smt2` file includes the following: ```lisp (= mode_1 2) (=...
I think there was a similar issue before when you introduce a variable behaving as `time`. Here is the `smt2` formula: ``` (set-logic QF_NRA_ODE) (declare-fun b () Real) (declare-fun b_0_0...
Hi, I am currently formalizing a simple system with ODEs in SMT2 and using dReal to solve it. I wanted to apply the invariant `not (x1)` to a particular mode...
- [ ] Single variable substitution - [ ] Print in infix form by default - [ ] Pretty-print all current constraints in the solver - [x] True and false
