diff --git a/src/math/polynomial/polynomial_factorization.cpp b/src/math/polynomial/polynomial_factorization.cpp index e0f050411..220048a9a 100644 --- a/src/math/polynomial/polynomial_factorization.cpp +++ b/src/math/polynomial/polynomial_factorization.cpp @@ -16,7 +16,7 @@ Author: Notes: [1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal, - 46(8-10):1853–1859, 1967. + 46(8-10):1853-1859, 1967. [2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third edition, 1997. [3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993. diff --git a/src/math/polynomial/polynomial_factorization.h b/src/math/polynomial/polynomial_factorization.h index 48b4efd98..f069121ba 100644 --- a/src/math/polynomial/polynomial_factorization.h +++ b/src/math/polynomial/polynomial_factorization.h @@ -16,7 +16,7 @@ Author: Notes: [1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal, - 46(8-10):1853–1859, 1967. + 46(8-10):1853-1859, 1967. [2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third edition, 1997. [3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993. diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index a1e28e727..230d352f3 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -16,7 +16,7 @@ Author: Notes: [1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal, - 46(8-10):1853–1859, 1967. + 46(8-10):1853-1859, 1967. [2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third edition, 1997. [3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993. diff --git a/src/math/polynomial/upolynomial_factorization.h b/src/math/polynomial/upolynomial_factorization.h index e687786da..327fffc9c 100644 --- a/src/math/polynomial/upolynomial_factorization.h +++ b/src/math/polynomial/upolynomial_factorization.h @@ -16,7 +16,7 @@ Author: Notes: [1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal, - 46(8-10):1853–1859, 1967. + 46(8-10):1853-1859, 1967. [2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third edition, 1997. [3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993. diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h index c076b2e6d..92d62301d 100644 --- a/src/math/polynomial/upolynomial_factorization_int.h +++ b/src/math/polynomial/upolynomial_factorization_int.h @@ -17,7 +17,7 @@ Author: Notes: [1] Elwyn Ralph Berlekamp. Factoring Polynomials over Finite Fields. Bell System Technical Journal, - 46(8-10):1853–1859, 1967. + 46(8-10):1853-1859, 1967. [2] Donald Ervin Knuth. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison Wesley, third edition, 1997. [3] Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Verlag, 1993. diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index 270e06f12..ecba3d598 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation Module Name: - dl_remation_manager.h + dl_relation_manager.h Abstract: @@ -316,7 +316,7 @@ namespace datalog { oldTgt:=tgt.clone(); tgt:=tgt \union src if(tgt!=oldTgt) { - delta:=delta \union src //also “delta \union tgt” would work + delta:=delta \union src //also ?delta \union tgt? would work } } @@ -488,7 +488,7 @@ namespace datalog { oldTgt:=tgt.clone(); tgt:=tgt \union src if(tgt!=oldTgt) { - delta:=delta \union src //also “delta \union tgt” would work + delta:=delta \union src //also ?delta \union tgt? would work } } diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h index 20d9ba6ef..b89603912 100644 --- a/src/smt/smt_model_finder.h +++ b/src/smt/smt_model_finder.h @@ -33,7 +33,7 @@ Abstract: Lugano, Switzerland, 2010. - Bugs, Moles and Skeletons: Symbolic Reasoning for Software - Development, Leonardo de Moura, Nikolaj Bjørner, IJCAR, + Development, Leonardo de Moura, Nikolaj Bjorner, IJCAR, Edinburgh, Scotland, 2010. Author: