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 ... 9
Title Δ
Defining a Theory of Sets with Z3/SMT-LIB2 0.00
Z3Py - Get all formulas containing an expression 0.00
Z3 / SMTLIB2 support for `distinct` 0.00
Shared libraries in Poly/ML 0.00
Error while including z3++.h 0.00
BitVector in Z3 - functions for different bits 0.00
Where to learn about z3 theorem prover APIs for c++? 0.00
Need help in using z3 API in a c++ program 0.00
Explosive memory use when reasoning about XOR (all AC theories?) 0.00
How to remove some duplicated expression using simplifying tactic i... 0.00
Getting concrete array values from a model 0.00
why this code returns Unsat? 0.00
what form of input does z3 smt solver take??can we use a file to re... 0.00
Create a constant bitvector +0.44
Z3py polish notation output 0.00
Finding the weakest precondition using z3py 0.00
Tracking z3 memory leaks 0.00
Getting concrete values from a model containing "array-ext" 0.00
Does Z3 have support for optimization problems -0.47
Z3 adding new variables during execution 0.00
Z3 Problems with push/pop with Python-API 0.00
PROOF_MODE affects outcome of check 0.00
Z3Py Bool variables cast to Int in the model 0.00
How to determine the number of solutions that a given instance has:... +0.47
Translating from Z3Py to SMT-LIB 0.00
eliminating forall using unsat 0.00
rewriting of Z3_ast during its traversing in C++ 0.00
using of z3_update_term function for term updating 0.00
Calculate minimum value of Bitvector in Z3 0.00
How to use Z3RCF-Py to prove that diff(x ^ 2 , x) = 2 when x = 1? 0.00
How to simplify the result of (eval (f x y))? 0.00
Simplex solver in Z3 0.00
Copying Z3 Solver 0.00
EPR formulas with equality and inequality 0.00
z3 timeout on nonlinear constraints 0.00
Incorrect Behavior for tactic solver for timeout 0.00
collection of variables in Z3 using C++ API 0.00
z3 variable naming standards 0.00
Accelerating the use of Z3py to check the satisfiability of a formula 0.00
Some proofs of validity using Z3 SMT 2.0 online 0.00
Using Z3Py online to prove that the derivative of x^2 is 2x +0.46
Get-assignment in Z3 0.00
Backtracking in Z3 increases the time to find the answer by the sol... 0.00
How do I get Z3 to return minimal model? 0.00
monitoring z3 memory usage characteristics 0.00
Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5 0.00
how to get the number of declare-funs in smt2 instance in z3(api) 0.00
how to assign new values to literals using z3 0.00
pretty printing Z3 with C APIs 0.00
Z3 Array in C language not python 0.00