Possible wrong answer in QF_BV #44
Comments
|
Thanks, fixed in unstable branch |
NikolajBjorner
added a commit
to NikolajBjorner/z3
that referenced
this issue
Apr 29, 2017
* local changes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add bound extraction for variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding fixed equality propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding fixed equality propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding fixed equality propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding bounds propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add eager bounds propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add configuration parameters for LP solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove wrong assert Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix wrong assert Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add timeout, signals to interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add stats Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * getting rid of typename Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * outline compound bound propagation functionality Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disable repropagation on pop Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add compound bound propagation code, remains disabled Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * stronger ad-hoc bounds propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * stronger ad-hoc bounds propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding validation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * check assignments and conflicts Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * check assignments and conflicts Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * relax assertion check to take care of cancellation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add debugging tracing to theory_lra to easier debug bounds propagation bug Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add debugging tracing to theory_lra to easier debug bounds propagation bug Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding fixed numeric bounds to fixed value table for better fixed equality propagation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add debugging to lra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial integration of opt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Closed
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
On problem https://gist.github.com/dddejan/89f6b9d3bc8084438178
z3: sat
yices2: unsat
cvc4: unsat
The text was updated successfully, but these errors were encountered: