search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

sat.euf #5573

Closed NikolajBjorner closed 2 years ago

NikolajBjorner commented 3 years ago

Known bug: quantifier instantiation is unsound (reports sat when unsat)

z3 C:/UF/grasshopper/instantiated/rec_reverse_acc_check_heap_access_17_4.smt2 sat.euf=true /st
NikolajBjorner commented 3 years ago

Known bug: E-matching is highly incomplete

z3 C:\uf\grasshopper\uninstantiated\concat_check_heap_access_23_4.smt2 smt.mbqi=false smt.auto_config=false sat.euf=true
NikolajBjorner commented 3 years ago

Known bug: Skolemization should be eagier, relevancy propagation doesn't work

z3 C:\UF\sledgehammer\Arrow_Order\smtlib.761827.smt2 /st smt.auto_config=false smt.mbqi=false sat.euf=true