Home
last modified time | relevance | path

Searched refs:ext_kid (Results 1 – 1 of 1) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_theorem_producer.cpp5130 const Expr& ext_kid = kid[0]; in getPlusTerms() local
5131 int size = d_theoryBitvector->BVSize(ext_kid); in getPlusTerms()
5143 plusTerms.push_back(ext_kid); in getPlusTerms()
5147 … plusTerms.push_back(d_theoryBitvector->newBVExtractExpr(ext_kid, extractLeft, extractRight)); in getPlusTerms()