Fixing more bugs in generating constraint and getting sat solution