]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e77ad2f) | patch
When using the SMT parser (x % 0) and (x /0) both evaluate to 1. This isn't in keepin...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 30 Aug 2009 10:44:51 +0000 (10:44 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 30 Aug 2009 10:44:51 +0000 (10:44 +0000)
commit22dd6033ea0dbd09600d4e2fe8353137f0506539
tree27202d54fdc0b6cf8af91010b78e18a5bbbdde1btree | snapshot
parente77ad2f363f66797fac28062b49b73bc0f416829commit | diff
When using the SMT parser (x % 0) and (x /0) both evaluate to 1. This isn't in keeping with the semantics of the SMTLIB language which says that the formula should only be satisfiable for all interpretations of division by zero (rather than just (x/0 ==1)).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@162 e59a4935-1847-0410-ae03-e826735625c1
src/AST/AST.cpp diff | blob | history
src/AST/ASTUtil.h diff | blob | history
src/AST/Transform.cpp diff | blob | history
src/bitvec/consteval.cpp diff | blob | history
src/parser/main.cpp diff | blob | history
STP Constraint Solver.