StackRating

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

Nikolaj Bjorner

Rating
1520.42 (31,060th) 		Reputation
7,321 (21,820th)
Page: 1 ... 4 5 6 7
Title Δ
Performance of the python Z3 API 0.00
Z3 prime numbers -4.23
Z3 is not able to prove the right-cancellation property in group th... +3.59
Building custom theories in Z3 0.00
Simplex Implementation in z3 0.00
Bizzare BitVector query slowness in presence of arrays 0.00
Validation query formulation, SMT solver, Z3, STP 0.00
Z3: Creating an enumerated type with number of items known dynamica... 0.00
Procedural Attachment in Z3 0.00
Z3: Does "qe" tactic preserve equivalence or only equisat... 0.00
z3: What might be the reason for timeout 0.00
How to define higher inductive types in Z3 0.00
How to efficiently solve combinations of theories in Z3 0.00
What is the most efficient way to encode pseudoboolean constraints... 0.00
Does Z3py support Linear Temporal logic LTL? 0.00
Z3 get-answer returns unsupported 0.00
How should I define a closed predicate? 0.00
Program satisfiability using Z3 0.00
Solvable queries in muZ 0.00
Converting to "set-option" SMTLib format -0.34
Cannot set pdr_use_farkas option in Z3py 0.00
Z3Py Fixedpoint computation too weak 0.00
Interpretation of Z3 Statistics 0.00
(apply qe) does not eliminate all quantifiers at once? 0.00
All possible values for a record datatype in Z3? 0.00
How to get different unsat cores when using z3 on logic QF_LRA 0.00
obtain the integer from a model after s.get_model() -2.30
Trying to implement GDL in z3 0.00
It is possible to compute the Kauffman bracket using Z3py? +3.78
Can I check whether a variable has deterministic value by C++ API 0.00
Can I get the path conditions from Pex in SMT 2 format? 0.00
Can get final CNF formula from Z3? 0.00
Can Z3 call python function during decision making of variables? 0.00
How to model signed integer with BitVector? +4.20
Quantifier elimination for multilinear rational arithmetic in Z3 0.00
How to solve a 2-SAT instance with 60 boolean variables and 99 clau... 0.00
slow invariant inference with Horn clauses in Z3 0.00
Why can't Z3/HORN solve xor? 0.00
Horn clauses in Z3 0.00
Simplification in z3 for implication 0.00
Satisfiability of Presburger Formulas with z3 0.00
How to make quantifier elimination using Z3-Py? 0.00
Z3 build error using Visual Studio compilers 0.00
Import Z3 into Visual Studio 2010 0.00
Simplify terms using SMT +3.92
How to get the model value in SAT problems using c++ api? 0.00
Z3Python: ForAll causes my code hangup, or returns Unsat, why? 0.00
Retrieve the bounds of an Extract node in z3py 0.00
How to solve a liars/truth-tellers instance using Z3Py and Z3 SMT-LIB 0.00
Prove 2 formulas equivalent under some conditions? 0.00