StackRating

An Elo-based rating system for Stack Overflow

Home | About | Stats and Analysis | Get a Badge

Rating Stats for

Taylor T. Johnson

Rating
1523.68 (25,662nd)

Reputation
2,460 (68,572nd)

Page: 1 2

Title	Δ
Z3: finding all possible solutions using C API	0.00
Z3 producing different models when run multiple times	+3.77
How much nonlinearity could z3 handle in practice?	0.00
Z3 : strange behavior with non linear arithmetic	0.00
Verification condition of an if-else and while loop in Z3	0.00
Incorrect result with Z3 SMT and Python	+3.74
Z3py returns unknown for equation using pow() function	0.00
Z3 support for square root	0.00
Z3 unsigned variables - simplify	0.00
Should Z3 prove monotonicity of <= (with respect to multiplicati...	0.00
z3 @ command line behaving differently than online	0.00
Z3: Covert int sort into bitvector	0.00
How to encode a fixed number of true variables?	0.00
Z3 Integer division not showing correct answer	0.00
Is this a bug for division in Z3?	0.00
Z3 Solver outputting the satisfying model?	0.00
z3 times out in case of a formula with quantifiers	0.00
(Z3Py) BitVec type conversion, "sort mismatch" error	0.00
Why does Z3 return "unknown" on this simple input?	0.00
How can I make a predefined Python function work with Z3py?	0.00
Or of bitvectors in z3Py	0.00
C# Z3 API calling problems in Visual studio 2012	0.00
It is possible to use LLVM Bytecode as Z3 input?	+1.80
Z3: Is it possible to simplify a part of the assertions only?	0.00
Z3: Use Java API to simplify assertions	0.00
Can z3 always give result when handling nonlinear real arithmetic	0.00
simplify and ctx-solver-simplify in Java (or C#)	0.00
integer division gives incorrect result	0.00
z3 solver: z3-SMT on Mac platform	0.00
Implement floor as an expression, not a statement	0.00
Combining nonlinear Real with linear Int	0.00
Model counting in Z3Py	0.00
How do I define for example a plus function on integers in Z3 using...	0.00
Is there a general way to add hypothetical assumptions in Z3?	0.00
z3 has unresolved symbols on Ubuntu 12.04 x86	0.00
z3 fails with this system of equations	+3.70
how to compute the number of total constraints in smtlib2 files in...	0.00
Why this code returns Unsat (formula using ForAll & Implies)?	0.00
Is there a way to obtain the default context in Z3?	0.00
Putting equality constraint in z3	0.00
Z3: how to Extract() from a constant number?	0.00
Can I use a SMT program's result in another SMT expression?	+4.05
Z3: Check if model is unique	0.00
Z3: Performing Matrix Operations	0.00
Repeating the matched models in Z3py	0.00
z3 number of solutions	0.00
Skolemization in Z3	0.00
Modeling memory access on Z3	0.00
Z3: finding all satisfying models	0.00
Can I use declare-const to eliminate the forall universal quantifier?	+3.96