pop takes a 2nd arg but push does not

ahumenberger / Z3.jl

Julia interface to Z3

MIT License

57 stars 7 forks source link

pop takes a 2nd arg but push does not #4

Closed shashi closed 4 years ago

shashi commented 4 years ago

but according to the spec they both do... Actually I'm not really sure what this number is supposed to be, but I'm suspecting it could be the cause of some crashes I'm seeing.

ahumenberger commented 4 years ago

I'm assuming you are talking about pop(::Solver, ::Int) and push(::Solver). These correspond to those from here: https://z3prover.github.io/api/html/classz3_1_1solver.html

push creates a backtracking point, and pop backtracks a certain amount of backtracking points.

shashi commented 4 years ago

Nice! Thank you again!