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 4 5 6 ... 7

Title	Δ
After changing from 4.3.2 to 4.4 I get often status UNKNOWN where I...	+0.48
Support for getting models when SAT (similar to --dump-models in CV...	0.00
Simplifying an expression leads to time out	-0.54
Z3py get_vars(f) equivalent for Java	0.00
Java API for z3 opt?	0.00
Build Z3 for StarExec	0.00
Defining functions on enumeration types in Z3	0.00
How can I access the variable mapping used when bit-blasting?	0.00
Automated tools for applying formal methods to verify security poli...	0.00
ForAll in Z3.py	0.00
Uninterpreted datatype in Z3	0.00
nuZ: What does the model say	0.00
nuZ: Use of soft-assertions with weights and ids	0.00
Cannot compile z3 library in Visual Studio 2008	0.00
Simplifying Z3 expressions	0.00
Z3 solver for string based constraints	0.00
z3: What might be the reason for timeout (rise4fun)	0.00
How to formulate summation in z3py	0.00
z3py cast constraint on number satisfiable of Exists	0.00
Z3: Fixed-size array of strings	0.00
How do I find the memory consumed in modeling/checking the satisfia...	-0.08
Difficulty in Storing Different sorts of Z3 expr into a map	0.00
Z3py SMT coding following variables and the formulas	0.00
Bi-implications in Z3.py	0.00
Use Z3 and SMT-LIB to define sqrt function with a real number	0.00
Z3: Difference logic performance	0.00
Z3 solver returning unsat when formula should be satisfiable	-0.52
Z3 MBQI different behavior between API and SMT-LIB for the same model	0.00
Understanding the index of all constants of a model	0.00
Z3 proofs: Are hypothesis and lemma rules always cleanly nested?	0.00
Why does Z3 return unknown result?	0.00
fixed points in Z3	0.00
Z3 Fixedpoints: What is the meaning of formula false in model?	0.00
Getting proof from z3py	0.00
Find the largest palindrome made from the product of two 5-digit nu...	0.00
Wrong result by ":arith.euclidean_solver true"	0.00
Different check-sat answers when asserting same property in between	-0.09
"context" cannot be constructed using c++ API in latest v...	0.00
Does Z3 support variable-only patterns in quantified formulas?	0.00
Z3 significance of Z3_get_ast_id	0.00
z3py throws parser error for a valid SMT2 file	+0.48
Extracting SMT-LIB Formula	0.00
Why does z3.check() slow when it is immediately preceded by z3.push...	0.00
Why is z3.And() slow?	0.00
Creating constant from sort in Z3 Python API	0.00
Z3 maximization API: switching objectives	0.00
How to quickly rename all variables in a formula with Z3 (python API)	0.00
Solving projection function equations using SMT in Z3	0.00
Disabling introduction of Skolem function in linear arithmetic proof	0.00
Z3 check whether two expressions are the same	0.00