StackRating

An Elo-based rating system for Stack Overflow
Home   |   About   |   Stats and Analysis   |   Get a Badge
Rating Stats for

Leonardo de Moura

Rating
1523.82 (25,453rd) 		Reputation
18,594 (7,475th)
Page: 1 2 3 4 5 6 7 ... 9
Title Δ
equivalence checking with Z3 0.00
Unprintable Solver.model() 0.00
Bug with check-sat when passed assumptions 0.00
Z3 Polarity using Z3 as SAT Solver 0.00
How does Z3 handle non-linear integer arithmetic? 0.00
Z3 patterns and injectivity 0.00
Learning Z3py - Is there support for arrays and loops 0.00
How to set the stacksize with C++11 std::thread 0.00
Z3 real arithmetics and data types theories integrating not that well 0.00
Z3 SMT 2.0 vs Z3 py implementation 0.00
An exception in z3 0.00
Custom simplifiers 0.00
Needless Var() returned by Solver.model() 0.00
Can I use Z3Py withouth doing a system-wide install? 0.00
z3 limitations in handling nonlinear real arithmetics 0.00
Can Z3 be used to preprocess problems? 0.00
declare-fun and define-fun in Z3 can't work together? 0.00
Installation of Z3 on a posix system without python? 0.00
Asymmetric behavior in ctx-solver-simplify -0.52
getting unsat core using Z3_solver_get_unsat_core 0.00
Using theory plugins with solvers 0.00
unsat core function in z3 0.00
How to use the annotation :no-pattern 0.00
z3 with SMTlib2 input 0.00
prevent solution from being simplified 0.00
Testing the (complete) instantiation strategy of Z3 0.00
Z3 python treats x**2 different than x*x? 0.00
Support for Multi-Dimensional Arrays in QF_AUFBV? 0.00
How to install iZ3? 0.00
How to use z3 split clauses of unsat cores & try to find out un... 0.00
Avoiding quantifiers in Z3 0.00
Setting tactic option in z3 +0.43
Z3 quantifier support 0.00
Z3 support of -m option 0.00
Proving inductive facts in Z3 0.00
Compiling Z3 test examples gives build error 0.00
z3 context reset API 0.00
Z3 maxsat smtlib 2.0 0.00
Generating data for the run of all possible paths in the program +0.48
FOL definitional theory in Z3 0.00
Error when building z3 on unix: cannot find -lrt 0.00
Compiling Z3 on a OSX 0.00
printing internal solver formulas in z3 0.00
datalog input format of Z3 -0.53
Quantifier Elimination for LIA in Z3 via C/C++ API +0.47
Z3 and DIMACS output 0.00
Getting 'sat' for large problems 0.00
Array select and store using the C++ API 0.00
Having trouble building Z3 in Visual Studio 0.00
mixing reals and bit-vectors 0.00