Lev Nachmanson

icon indicating a website link http://research.microsoft.com/en-us/um/people/levnach/

icon company Microsoft icon location Redmond, WA, US

Results 5 issues of Lev Nachmanson

Faster gc

Use polarity of the non-basic variables to create bounds on basic variables in Gomory cuts

comparing smt.arith.solver=2 and smt.arith.solver=6

2 comment

Experimenting on QF_NIA/20170427-VeryMax/CInteger/Stroeder_15__GulwaniJainKoskinen-PLDI2009-Fig1_true-termination.c__p23650_edge_closing_0.smt2. The legacy solves it in seconds, the new one takes at least more than 10 minutes. In a good run legacy creates :arith-tableau-max-columns 355 :arith-tableau-max-rows 59 The...

Arithmetic

port sample cell projection

revert the behavior of add_zero_assumption

nlsat produces an unsound lemma

It happens in commit 11fb5c7dc49d879cdc2a3c3c4a732cd3c39749c5 on a Mac. Steps to reproduce: Build the release. Run ./z3 ~/dev/current/7489.smt2 tactic.default_tactic=smt nlsat.log_lemmas=true -T:5 >& /tmp/lemmas7489.smt2 It produces lemma 114 :!(x0 > 0) or...