StackRating

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

Leonardo de Moura

Rating
1523.82 (25,453rd) 		Reputation
18,594 (7,475th)
Page: 1 ... 6 7 8 9
Title Δ
Quantifiers and patterns (QBF formula) 0.00
Quantifier Vs Non-Quantifier 0.00
Reading a Z3 file 0.00
Does not 'check-sat' support Boolean function as assumption? 0.00
Input arguments of Z3_benchmark_to_smtlib_string() 0.00
Specifying initial model values for Z3 0.00
Does variables with large integer values affect the performance of... 0.00
Why does Z3's `get-value` return an expression instead of concrete... 0.00
Exclusion and inclusion in Z3 0.00
Sort-parametric wrapper functions 0.00
Can the output of intermediate models be disabled? 0.00
Z3: models with Reals 0.00
Z3 Context serialization/deserialization? 0.00
Does pull_nested_quantifiers option work with simplify in Z3? 0.00
Is z3_dbg.dll still part of the distribution? 0.00
Getting a "good" unsat-core with z3 (logic QF_BV) 0.00
SMTLIB array theory oddity in Z3 0.00
soundness issue with integer/bv mixed benchmarks? 0.00
a datatype contains a set in Z3 -4.18
z3: how to convert a boolean sort into a bit vector sort 0.00
Reason for timeout? 0.00
Symmetry breaking for Z3 -- in the context of the UFBV logic (new v... 0.00
z3 timeout on linux/mac 0.00
how do i invoke Z3 Programmatically 0.00
What is the reason behind the warning message in Z3: "failed t... 0.00
Incremental calls to Z3 on UFBV with and without push calls 0.00
Can Z3 work in incremental mode? 0.00
Counterexample output of Z3 0.00
Z3 Segmentation Fault 0.00
Multiset Partition Using Linear Arithmetic and Z3 -0.23
Can't generate a model with Z3 0.00
Same input, Z3 works on Windows, but gives Segmentation Faults on L... 0.00
Wrong result from z3 0.00
How to invoke Z3 on an input file 0.00
How to find out if a z3_ast corresponds to a clause? 0.00
About the representation of the Uninterpreted Function in Z3 +3.92
Is there any difference between Z3 versions 2.19 and 3.2 w.r.t. SMT... 0.00
Sort Mismatch in Model 0.00
Values for Array Terms in z3 Models 0.00
How do I find the memory and time required for modeling/checking th... 0.00
Can Z3 handle datatypes that contains sorts introduced by declare-s... 0.00
Soft/Hard constraints in Z3 0.00
Use Z3 and smtlib to calculate configuration/model with mixed values +4.13
Expressing a subtype relation between enumeration types in Z3 0.00
Use of term rewriting in decision procedures for bit-vector arithme... +4.00
Is there an option to pretty-print bit vectors as signed decimals? 0.00
Is there any way to simplify the path conditions 0.00
The "pull-nested-quantifiers" option seems to cause probl... 0.00
How are Int sort (of SMT-LIB 2.0 Ints theory) and dynamically decla... 0.00
Display quantified-out formula 0.00