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 ... 9
Title Δ
z3 behaviour changing on request for unsat core 0.00
What are the limits of reasoning in quantified arithmetic in SMT? +2.50
Z3 Theory Plugins splitting to sub-problems 0.00
Iteratively declaring distinct variables 0.00
Using quantifer elimination with Z3 Python 0.00
SegFault when using quantifier elimination in Z3 +0.43
How to implement array of bitvectors in z3's Python APIs 0.00
Z3 formula fails syntatic check 0.00
Encoding returns "unknown" 0.00
Z3: convert Z3py expression to SMT-LIB2 from Solver object 0.00
Finding BitVec weight efficently (aka access to bits of a bitvector... +0.46
Solver timeout within loop using z3 Python API 0.00
how to convert expression to string in z3 0.00
z3 pseudo-randomly hangs while parsing through a SAT Model 0.00
Z3: convert Z3py expression to SMT-LIB2? 0.00
Pickling Z3 Python Objects 0.00
Z3py: how to extend and trunc variables? 0.00
Unsatisfiable Cores in Z3 Python 0.00
Z3 4.3: get complete model +0.49
Z3: finding all possible values of a variable 0.00
Z3 tactic for finding partial assignment 0.00
In Z3, what's the most efficient way to describe this in array theo... 0.00
UNKNOWN when using def's 0.00
Use Z3 managed API on Mono 0.00
Z3/SMT: When should I prefer push/pop to reset? 0.00
set operations over Z3 expressions 0.00
Can I set the priority of boolean variables in z3? 0.00
z3python: no XOR operator? 0.00
Optimising z3 input 0.00
Is calling check twice supposed to work? 0.00
retrieving value of an enumerated type in Z3Py 0.00
How does Z3 deal with forall proposition with uninterpreted functio... 0.00
substitution in Z3Py 0.00
z3 C++ API & ite 0.00
Can z3 read the outputfile of MathSAT as its inputfile? 0.00
Check if a formula is a term in Z3Py -0.01
Building z3 on mac os x 0.00
Does Z3 support to encode array of Objects? 0.00
Z3py: how to get the list of variables from a formula? 0.00
Prove() method, but ignore some 'free' variables? -0.03
Z3 Setting Random Seed using C-API 0.00
simplification in Z3 0.00
Satisfiablity checking in non-linear integer arithmetic by approxim... 0.00
how to eliminate bitvector arithmetic in Z3 0.00
What happened to the custom theory solver methods in the Z3 API? 0.00
Prove() method of Z3? 0.00
Reducing the number of used clauses using proof goal in Z3 0.00
converting IR to Z3 formula? 0.00
How to use z3 incrementally and model without propositional value ？ 0.00
how to set timeout for z3_solver using C-API? 0.00