mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 00:41:56 +00:00
Code Activity

notes

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-29 04:52:51 -07:00
parent 81cffee736
commit eff17a6252
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nla_stellensatz.cpp
View file

@ -49,11 +49,13 @@ Currently missed lemma:
(46) - j5 + j23 + j27 >= 0 (46) - j5 + j23 + j27 >= 0
(44) j4 - j7 - j25 >= 0 (44) j4 - j7 - j25 >= 0
j4 - j7 - j27 >= 1 j4 - j7 - j27 >= 1 (from (51) + (46))
j4 - j5 - j7 + j23 >= 1 (from (46)) j4 - j5 - j7 + j23 >= 1 (from (46))
j4 - j5 + j23 >= 2 j4 - j5 + j23 >= 2 (from (12))
j4 - j5 + j11 >= 2 j4 - j5 + j11 >= 2 (from (38))
j4 - j5 >= 3 j4j4 - j4j5 + j4j11 >= 2j4 (multiply by j4)
j4j11 >= 2j4 (subtract 10 multiplied by j4)
..
.. ..
*/ */