]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cb9e1cb) | patch
Fixed correctness bug in TermToConstTermUsingModel. CounterExampleMap
authorkatelman <katelman@e59a4935-1847-0410-ae03-e826735625c1>
Tue, 30 Dec 2008 06:17:29 +0000 (06:17 +0000)
committerkatelman <katelman@e59a4935-1847-0410-ae03-e826735625c1>
Tue, 30 Dec 2008 06:17:29 +0000 (06:17 +0000)
commit00cfb06c78c2614907f3d42950f99419e47ccfc1
tree5c4befce2b05207b578613372acbc1f71b8ffe88tree | snapshot
parentcb9e1cbfa9e4c53108e56fd671f02aa2052d53bacommit | diff
Fixed correctness bug in TermToConstTermUsingModel. CounterExampleMap
originally gets a copy of SubstitutionMap by way of SolverMap, and since
SubstitutionMap may not have fully reduced terms, we need to call
TermToConstTermUsingModel on anything read from CounterExampleMap. This was not
done for an array read case.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@48 e59a4935-1847-0410-ae03-e826735625c1
AST/ToSAT.cpp diff | blob | history
STP Constraint Solver.