![]() |
|
|---|
examples\C_API contains the shell script build.sh to build the test application using gcc.__cdecl).z3.dll and z3_dbg.dll?z3_dbg.dll contains assertion checking. You can use it to check whether you are using the API correctly or not./rd: and /rs. These options control the randomization in Z3. Example: z3 -rd:5 -rs:100 -st withOpt.smt2
unknown in some problems containing quantifiers?unknown. Recall that there is no sound and complete procedure for first-order logic formulas of linear arithmetic with uninterpreted function symbols.(set-option :produce-unsat-cores true) (declare-fun x () (_ BitVec 32)) (declare-fun y () (_ BitVec 32)) (assert (! (not (not (= x #x00000000))) :named a1)) (assert (! (not (= y #x00000000)) :named a2)) (assert (! (not (= x #x00000000)) :named a3)) (check-sat) (get-unsat-core)