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 ... 7
Title Δ
Compute recursive functions with Z3 0.00
How to add toUpperCase function in Z3? 0.00
How to deal with recursive function in Z3? 0.00
Z3Py: getting the function corresponding to each operator e.g. '... -2.01
Z3Py: Why are the following assumptions not satisfiable? 0.00
QF_NIA script terminates instantly with Z3 4.3.2, but not with 4.4.2 0.00
Assumptions in Z3 or Z3Py -0.11
Can we use ite expression in Z3 fixed-poin query 0.00
Stochastic Satisfiability Modulo Theory +1.91
Z3 Power Modulo Statements 0.00
z3 variable types switching 0.00
Z3 String/Char xor? 0.00
Equal lists are permutations of one another. Why does Z3 answer ... 0.00
OCaml bindings for Z3: support for String sorts 0.00
get intermediate results from z3opt 0.00
Datatypes with functions as attributes in Z3 Python 0.00
Z3Opt: Finding a sub-optimal model within a time bound? 0.00
How to prove two relations equal in Z3 using HORN logic -0.03
How is model generated with Z3? 0.00
z3 minimization and timeout 0.00
"unknown sort" error in fixed point queries 0.00
Bug in Z3 Datalog 0.00
Z3 BitVector bug? 0.00
Segfault in bv_rewriter::mk_mul_eq() 0.00
Evaluate a Z3 expression 0.00
z3: A formula and its negation are unsatisfiable 0.00
C# Z3 (Version 4.3) ParseSMTLIB2String says "unsupported" 0.00
Why does creating And/Or objects in Z3py take more time than expect... 0.00
Z3 fractional exponent bug (maybe) 0.00
Cartesian product in Z3 +1.92
How to get the variable list from a z3 formula? 0.00
How to transform a arithmetic expression to a Python arithmetic fun... -0.56
Is support for recursive functions on the roadmap for Z3? 0.00
z3 UNSAT, how to retrieve multiple cores 0.00
Z3 Time Restricted Optimization 0.00
Z3 enumsort update 0.00
Number of variables in Z3 statistics 0.00
How to get z3 to return multiple unsat cores, multiple satisfying a... 0.00
Arithmetic operation on Z3 bool variable 0.00
SIGBUS crash on Solaris 8 0.00
Code changes to build z3 on Solaris 0.00
z3Opt optimize non-linear function using qfnra-nlsat 0.00
How to simplify the union of two expressions: Z3 solver 0.00
Convert SMT-LIBv2 QF_AUFBV to CNF DIMACS format using Z3 0.00
Z3 install error: datalog_frontend.cpp NMAKE : fatal error U1077 fr... 0.00
How to extract from a bit-vector using parameters with "Int&qu... 0.00
Use Z3 to determine difficulty of quantifier elimination for BV-que... 0.00
z3, z3py: Is it possible to intrinsically reduce the search space o... +0.47
Z3 : Encoding functions whose ranges are set of subsets 0.00
Can I find the shortest path via Z3 0.00