mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

remove comment about bug in forbidden_intervals, it is correct there, but maybe a bug in viable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-03 08:02:02 -08:00
parent eda3cac8d4
commit 9572623675
1 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/forbidden_intervals.cpp
View file

@ -285,12 +285,6 @@ namespace polysat {
* Match e1 + t <= e2, with t = a1*y
* condition for empty/full: e2 == -1
*/
// NSB - bug?
// what happens when a1 != 1 and a1 != -1?
// if a1 is even is this still correct?
// example: match_linear1 12 v81 + -1*v20*v12 == 0 [v81 + 1 ; v81[ := [1;0[ v20 + -532 == 0 v81 == 0
// from bench25.smt2
//
bool forbidden_intervals::match_linear1(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,