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 2 3 ... 7
Title Δ
Which encodings are preferable to use Z3 to solve a partial order t... -0.07
What are the equivalent horn clauses to these clauses? 0.00
Why does Z3 return Unknown for these horn clauses 0.00
Nonzero vector in quantifier +1.85
Unexpected unknown with ill-defined function definition axiom 0.00
Z3: Hamming Distance between two bit vectors -0.16
How to detect or prove the recurrence relations is periodic sequenc... -0.16
Set pretty printer line width in Z3's C++ API 0.00
What is the difference between BitVec and BitVecVal in z3 0.00
z3 Regex sort unrecognized 0.00
Z3-OPT binary files for the windows 64 bit machine 0.00
Printing z3 expressions using the python api 0.00
How to verify loop with z3? 0.00
Iterating over unsat cores 0.00
Symbol Creation in Z3 Java API 0.00
How to check in Z3py whether the expression contains a conditional... 0.00
Fully evaluated results in Z3? 0.00
function with quantifier in Z3 +0.47
Unable to extract value for Z3 EnumSort in z3py 0.00
Z3PY equation, size limitation 0.00
Missing (str.to-int s) in Z3 4.5.1 0.00
SMT solver with custom theories? 0.00
Workaround for z3 not supporting injectivity 0.00
Z3 invalid function app, args missing 0.00
Does the order of prenex quantification matter in EPR fragment? 0.00
Windows: Z3Exception("init(Z3_LIBRARY_PATH) must be invoked be... -0.18
Z3 Strings: finding the API 0.00
Check function while "QF_FD" logic is set throws AccessVi... +1.84
Setting logic in Z3 .Net API -0.02
z3py compare Datatype / Enum to string -0.52
Set Bit at Index i in Z3 -0.16
Z3 low cpu usage 0.00
z3 c++ api modulo operation with integer 0.00
Creating formula taking too much time in Z3py 0.00
Taking the floor of a real number in Z3Py 0.00
Why can't Z3 propose a sort with no elements? 0.00
Mutually recursive datatypes in z3 and their interaction with built... 0.00
Howt to use properly ZeroExt(n,a) in a Z3py formula? 0.00
Declare matrix with unknown size in Z3 -0.04
how to duplicate a solver created in pysmt? 0.00
Z3 getting last valid model +0.46
Z3 API: Crash when parsing fixed point SMTLib string 0.00
Mysterious "unabled nested data-type expression" in Z3 0.00
Bug with recursive functions? 0.00
Can I read a SMT2 file into a solver through the z3 c++ interface? 0.00
Z3 C++ API yeilds "unknown" while binary on serialized ou... 0.00
Is it possible to prove mathematical statements including factorial... +0.30
partial assignments in Z3 0.00
Is there a way to use a maximize/ minimize objective with Z3 solver... 0.00
Optimize in Z3 .NET API giving incorrect results - bug? 0.00