{var%20f='http://v.t.sina.com.cn/share/share.php?appkey=1515056452',u=z||d.location,p=['&url=',e(u),'&title=',e(t||d.title),'&source=',e(r),'&sourceUrl=',e(l),'&content=',c||'gb2312','&pic=',e(p||'')].join('');function%20a(){if(!window.open([f,p].join(''),'mb',['toolbar=0,status=0,resizable=1,width=440,height=430,left=',(s.width-440)/2,',top=',(s.height-430)/2].join('')))u.href=[f,p].join('');};if(/Firefox/.test(navigator.userAgent))setTimeout(a,0);else%20a();})(screen,document,encodeURIComponent,'','','https://www.manongdao.com/data/attach/logo/logo.png', '推荐 萌系小妹纸 的问题《z3Opt optimize non-linear function using qfnra-nls》','https://www.manongdao.com/q-835241.html','页面编码gb2312|utf-8默认gb2312'));){kind=link}
I'm trying to use z3Opt for optimizing a real non-linear function, but even for simple cases like the following one
http://rise4fun.com/Z3Opt/JbaU
the result is not what it is expected to be. It's like z3 it is not optimizing at all.... anyone can help me understand?
Optimization of non-linear functions is not supported at this point, so no guarantee is given on results. It would probably be better if the solver returns unknown (and not sat) for this case, which is something I should look into.